149 citations · 563 across the 54 of their papers we have counts for
Showing 2013 · cs.AIShow all
3 papers · 2 filters
cs.AI2013★ 94 cited
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…
cs.AI2013
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…
cs.AI2013★ 5 cited
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…