149 citations · 825 across the 48 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…
MaLeS: A Framework for Automatic Tuning of Automated Theorem Provers
Daniel Kühlwein, Josef Urban
MaLeS is an automatic tuning framework for automated theorem provers. It provides solutions for both the strategy finding as well as the strategy scheduling problem. This paper des…
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…