Description of HolyHammer


HOLyHammer is a machine learning for theorem proving framework.
It allows the a user of a proof assistant to call external provers
such as E, Vampire and Z3 using a limited number of premises
selected by a machine learning algorithm.

Development Timeline

- 2012-2014: HolyHammer for HOL/Light.
This is the project of J.Urban and C.Kaliszyk.
More information.
- 2015: HolyHammer for HOL4 (shared code base with HOL/Light)
- 2017: Premise selection ported to HOL4
- 2018: HOL to FOL translation ported to HOL4
- 2019: Translations to many TPTP formats

The current implementation of HolyHammer for HOL4 is included
in the HOL4 distribution.

Results re-proving the HOL4 standard library

Date Dataset Parameters Evaluated Proven Reconstructed (1s)
27/05/19 standard library E prover auto-schedule 12069 3675 (30.4%) 3430 (28.4%)


5s, human dep