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.
- 2012-2014: HolyHammer for HOL/Light.
This is the project of J.Urban and C.Kaliszyk.
- 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.
|27/05/19||standard library||E prover auto-schedule||12069||3675 (30.4%)||3430 (28.4%)|
|5s, human dep|