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.
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.
| Date | Dataset | Parameters | Evaluated | Proven | Reconstructed (1s) |
|---|---|---|---|---|---|
| 27/05/19 | standard library | E prover auto-schedule | 12069 | 3675 (30.4%) | 3430 (28.4%) |
|
3971206043e478ced916b0f9bfafd03a890441a4 |
5s, human dep |