NameDateSize

..25-Jul-201970

.gitignoreH A D25-Jul-2019112

COPYRIGHTH A D25-Jul-20191.5 KiB

examples/H25-Jul-20194

hhReconstruct.sigH A D25-Jul-2019403

hhReconstruct.smlH A D25-Jul-20192.7 KiB

hhTptp.sigH A D25-Jul-2019326

hhTptp.smlH A D25-Jul-20195.5 KiB

hhTranslate.sigH A D25-Jul-20191.6 KiB

hhTranslate.smlH A D25-Jul-201913.1 KiB

hhWriter.sigH A D25-Jul-2019417

hhWriter.smlH A D25-Jul-201914 KiB

HolmakefileH A D25-Jul-2019278

holyHammer.sigH A D25-Jul-20192.3 KiB

holyHammer.smlH A D25-Jul-201914.4 KiB

legacy/H25-Jul-20194

provers/H25-Jul-20195

READMEH A D25-Jul-20191.3 KiB

selftest.smlH A D25-Jul-201929

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