149 citations · 563 across the 54 of their papers we have counts for
5 papers · 1 filter
MizAR 40 for Mizar 40
Cezary Kaliszyk, Josef Urban
As a present to Mizar on its 40th anniversary, we develop an AI/ATP system that in 30 seconds of real time on a 14-CPU machine automatically proves 40% of the theorems in the lates…
Lemma Mining over HOL Light
Cezary Kaliszyk, Josef Urban
Large formal mathematical libraries consist of millions of atomic inference steps that give rise to a corresponding number of proved statements (lemmas). Analogously to the informa…
HOL(y)Hammer: Online ATP Service for HOL Light
Cezary Kaliszyk, Josef Urban
HOL(y)Hammer is an online AI/ATP service for formal (computer-understandable) mathematics encoded in the HOL Light system. The service allows its users to upload and automatically…
Proceedings 10th International Workshop On User Interfaces for Theorem Provers
Cezary Kaliszyk, Christoph Lüth
This EPTCS volume collects the post-proceedings of the 10th International Workshop On User Interfaces for Theorem Provers (UITP 2012), held as part of the Conferences on Intelligen…
Formal Mathematics on Display: A Wiki for Flyspeck
Carst Tankink, Cezary Kaliszyk, Josef Urban +1
The Agora system is a prototype "Wiki for Formal Mathematics", with an aim to support developing and documenting large formalizations of mathematics in a proof assistant. The funct…