149 citations · 563 across the 54 of their papers we have counts for
4 papers · 1 filter
Premise Selection and External Provers for HOL4
Thibault Gauthier, Cezary Kaliszyk
Learning-assisted automated reasoning has recently gained popularity among the users of Isabelle/HOL, HOL Light, and Mizar. In this paper, we present an add-on to the HOL4 proof as…
Sharing HOL4 and HOL Light proof knowledge
Thibault Gauthier, Cezary Kaliszyk
New proof assistant developments often involve concepts similar to already formalized ones. When proving their properties, a human can often take inspiration from the existing form…
Proceedings Fourth Workshop on Proof eXchange for Theorem Proving
Cezary Kaliszyk, Andrei Paskevich
This volume of EPTCS contains the proceedings of the Fourth Workshop on Proof Exchange for Theorem Proving (PxTP 2015), held as part of the International Conference on Automated De…
A formal proof of the Kepler conjecture
Thomas Hales, Mark Adams, Gertrud Bauer +19
This article describes a formal proof of the Kepler conjecture on dense sphere packings in a combination of the HOL Light and Isabelle proof assistants. This paper constitutes the…