Name | Date | Size | ||
---|---|---|---|---|
.. | 25-Jul-2019 | 70 | ||
.gitignore | H A D | 25-Jul-2019 | 112 | |
COPYRIGHT | H A D | 25-Jul-2019 | 1.5 KiB | |
examples/ | H | 25-Jul-2019 | 4 | |
hhReconstruct.sig | H A D | 25-Jul-2019 | 403 | |
hhReconstruct.sml | H A D | 25-Jul-2019 | 2.7 KiB | |
hhTptp.sig | H A D | 25-Jul-2019 | 326 | |
hhTptp.sml | H A D | 25-Jul-2019 | 5.5 KiB | |
hhTranslate.sig | H A D | 25-Jul-2019 | 1.6 KiB | |
hhTranslate.sml | H A D | 25-Jul-2019 | 13.1 KiB | |
hhWriter.sig | H A D | 25-Jul-2019 | 417 | |
hhWriter.sml | H A D | 25-Jul-2019 | 14 KiB | |
Holmakefile | H A D | 25-Jul-2019 | 278 | |
holyHammer.sig | H A D | 25-Jul-2019 | 2.3 KiB | |
holyHammer.sml | H A D | 25-Jul-2019 | 14.4 KiB | |
legacy/ | H | 25-Jul-2019 | 4 | |
provers/ | H | 25-Jul-2019 | 5 | |
README | H A D | 25-Jul-2019 | 1.3 KiB | |
selftest.sml | H A D | 25-Jul-2019 | 29 |
README
1HOLyHammer is a machine learning for theorem proving framework. 2 3Install Holyhammer: 4 5 Run Holmake in src/holyhammer (done during the build) 6 7Install external provers: Eprover(1.8 1.9 2.0, latest version should work too), 8 Z3 (4.0), Vampire (4.2.2) 9 10 1) Download provers 11 - Eprover 2.0: 12 Source: http://wwwlehre.dhbw-stuttgart.de/~sschulz/E/E.html 13 (eprover binary found in PROVER directory) 14 - Z3 4.0 (not 4.4.0): 15 Binaries: http://isabelle.in.tum.de/components/ 16 - Vampire 4.2.2: 17 Linux binary: https://vprover.github.io/download.html 18 Source: https://github.com/vprover/vampire 19 (produces vampire_rel_master_3993 in the top directory) 20 2) Prover binaries with the appropriate version should be copied or linked 21 in the directory src/holyhammer/provers. 22 They should be respectively renamed to eprover, z3 and vampire. 23 3) Make sure you have the permission to execute them (chmod +x) 24 25Example: 26 27 load "holyHammer"; 28 open holyHammer; 29 holyhammer ``1+0=1``; 30 31 Loading 2995 theorems 32 vampire found a proof 33 z3 found a proof 34 eprover found a proof 35 METIS_TAC [arithmeticTheory.ALT_ZERO, arithmeticTheory.NUMERAL_DEF, 36 arithmeticTheory.SUC_ONE_ADD, numeralTheory.numeral_suc] 37 38Questions: 39 40 If you have any question, you can send an email to 41 email@thibaultgauthier.fr 42 43