-
Notifications
You must be signed in to change notification settings - Fork 6
/
README
127 lines (91 loc) · 3.85 KB
/
README
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
2015.05.25
README file for Zenon Modulo 0.4.2
----------------------------------------
For license information, see LICENSE
----------------------------------------
Contact: Pierre Halmagrand <[email protected]>
Guillaume Bury <[email protected]>
Raphael Cauderlier <[email protected]>
----------------------------------------
Prerequisites:
- OCaml 4.02.1 (with ocamlopt)
- Coq 8.0.x
- Dedukti 2.3
- zarith 1.3
- ImageMagick (optional)
- Ghostscript (optional)
----------------------------------------
Compile and install with:
configure
make
make install
----------------------------------------
Remarks:
- Zenon Modulo is an automated theorem prover for classical
first order logic with polymorphic types
- Zenon Modulo can be download at:
https://www.rocq.inria.fr/deducteam/ZenonModulo/index.html
https://gforge.inria.fr/projects/zenon/
- Zenon Modulo is part of the BWare project
http://bware.lri.fr/
- Zenon Modulo is used in FoCaLiZe project
http://focalize.inria.fr/
- Proceedings about Zenon Modulo may be found here
http://hal.inria.fr/hal-00909784
http://hal.inria.fr/hal-00909688
http://hal.inria.fr/hal-01171360
- Zenon Modulo accepts input files with the TPTP syntax (FOF and TFF1)
http://www.cs.miami.edu/~tptp/
And also with Dedukti syntax
http://dedukti.gforge.inria.fr/
- Zenon Modulo may produce proof certificates for Dedukti
http://dedukti.gforge.inria.fr/
https://gforge.inria.fr/projects/dedukti/
- To use Zenon Modulo with TFF1 files of the BWare Proof Obligations
(with B set theory express in B_modulo.why):
>> activate the '-b-rwrt' flag to build the rewrite system
>> activate the '-rwrt' flag to transform more axioms into rewrite rules
>> activate the '-x arith' flag to use the arithmetic extension
>> activate the '-odk' flag to generate a proof certificate for dedukti
>> activate the '-om' flag to print a proof
- To use Zenon Modulo with Dedukti files for FoCaLiZe project
>> activate the '-idk' flag to read input in Dedukti format
>> activate the '-x focal' flag to load FoCaLiZe extension (for dealing with booleans and pairs)
>> activate the '-odkterm' flag to get a Dedukti term as output
----------------------------------------
Examples:
First, compile Dedukti files:
$ dkcheck -e cc.dk dk_bool.dk dk_logic.dk dk_tuple.dk basics_minimal.dk modulogic.dk zenon_focal.dk
1/ BWare with TFF1 files
Some TFF1 input files are given as examples into ./examples repository
Four of them are set properties coming from the B-Book, and the last one
is a Proof Obligation coming from the BWare benchmark.
To run and test Zenon Modulo:
- Minimal call
$ zenon_modulo -itptp -b-rwrt ./examples/file_name.p
- Print proof and search information
$ zenon_modulo -itptp -b-rwrt -vv 4 -om ./examples/file_name.p
- Generate proof certificate for Dedukti
$ zenon_modulo -itptp -b-rwrt -odk ./examples/file_name.p > certificate.dk
- To verify the proof with Dedukti
$ dkcheck certificate.dk
2/ FoCaLiZe with Dedukti files
An example of a problem written in Dedukti syntax and using the
FoCaLiZe extension is also given in the ./examples repository
To run it:
$ zenon_modulo -idk -x focal ./examples/bool_and_commute.coz -odkterm > bool_and_commute.dk
and then paste the given Dedukti term in a Dedukti file wich contains the problem statement:
#NAME bool_and_commute.
bool := basics.bool__t.
bool_and_commute : dk_logic.eP (
dk_logic.forall
bool
(b1 : cc.eT bool =>
dk_logic.forall
bool
(b2 : cc.eT bool =>
dk_logic.equal bool
(basics._amper__amper_ b1 b2)
(basics._amper__amper_ b2 b1))))
:= <the given term>.
----------------------------------------