149 citations · 563 across the 54 of their papers we have counts for
Showing 2012Show all
2 papers · 1 filter
cs.AI2012★ 149 cited
Learning-Assisted Automated Reasoning with Flyspeck
Cezary Kaliszyk, Josef Urban
The considerable mathematical knowledge encoded by the Flyspeck project is combined with external automated theorem provers (ATPs) and machine-learning premise selection methods tr…
cs.LO2012★ 35 cited
General Bindings and Alpha-Equivalence in Nominal Isabelle
Christian Urban, Cezary Kaliszyk
Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem prover. It provides a proving infrastructure for reasoning about programming language calculi involving nam…