1ZENON(1)                         User Commands                        ZENON(1)
2
3
4

NAME

6       zenon - Automated theorem prover for first-order classical logic
7

SYNOPSIS

9       zenon [OPTIONS] FILE
10

DESCRIPTION

12       Zenon  is  an  automated theorem prover for first order classical logic
13       with equality, based on the tableau method.  Zenon can read input files
14       in TPTP, Coq, Focal, and its own Zenon format.  Zenon can directly gen‐
15       erate Coq proofs (proof scripts or proof terms),  which  can  be  rein‐
16       serted into Coq specifications.  Zenon can also be extended.
17

OPTIONS

19       If file is "-", it will read input from stdin.
20
21       -context  provide context for checking the proof independently
22
23       -d        debug mode
24
25       -errmsg <message>
26                 prefix warnings and errors with <message>
27
28       -help, --help
29                 print this option list and exit
30
31       -I <dir>  add <dir> to the include path (for TPTP input format)
32
33       -icoq     read input file in Coq format
34
35       -ifocal   read input file in Focal format
36
37       -itptp    read input file in TPTP format
38
39       -iz       read input file in Zenon format (default)
40
41       -loadpath path to Zenon's coq libraries (default /usr/share/zenon)
42
43       -max <s>[kMGT]/<i>[kMGT]/<t>[smhd]
44                 set size, step, and time limits
45
46       -max-size <s>[kMGT]
47                 limit  heap  size  to  <s>  kilo/mega/giga/tera word (default
48                 100M)
49
50       -max-step <i>[kMGT]
51                 limit number of steps  to  <s>  kilo/mega/giga/tera  (default
52                 10k)
53
54       -max-time <t>[smhd]
55                 limit CPU time to <t> second/minute/hour/day (default 5m)
56
57       -ocoq     print the proof in Coq script format
58
59       -ocoqterm print the proof in Coq term format
60
61       -oh       <n>              print  the  proof in high-level format up to
62                 depth <n>
63
64       -ol       print the proof in low-level format
65
66       -olx      print the proof in raw low-level format
67
68       -om       print the proof in middle-level format
69
70       -onone    do not print the proof (default)
71
72       -opt0     do not optimise the proof
73
74       -opt1     do peephole optimisation of the proof (default)
75
76       -p0       turn off progress bar and progress messages
77
78       -p1       display progress bar (default)
79
80       -p2       display progress messages
81
82       -q        (quiet) suppress proof-found/no-proof/begin-proof/end-proof
83
84       -rename   prefix all input symbols to avoid clashes
85
86       -rnd <seed>
87                 randomize proof search
88
89       -stats    print statistics
90
91       -short    output a less detailed proof
92
93       -v        print version string and exit
94
95       -versions print CVS version strings and exit
96
97       -w        suppress warnings
98
99       -where    print the location of the zenon library and exit
100
101       -wout <file>
102                 output errors and warnings to <file> instead of stderr
103
104       -x <ext>  activate extension <ext>
105
106

EXAMPLE

108       The command:
109                zenon -itptp -ocoq /usr/share/zenon*/examples/tptp-COM003+2.p
110       will take the input file "tptp-COM003+2.p"  in  TPTP  format  (-itptp),
111       search for a proof, and produce any proof output in Coq format (-ocoq).
112       tptp-COM003+2.p is a TPTP representation of the halting problem.  Zenon
113       can prove this, and will print out:
114              (* PROOF-FOUND *)
115              (* BEGIN-PROOF *)
116              ... details of proof in Coq format
117              (* END-PROOF *)
118
119

SEE ALSO

121       zenon-format(5)
122
123

AUTHOR

125       This man page was written by David A. Wheeler.
126

128       Zenon  is  released  under  the  revised BSD license.  This man page is
129       released under both the revised BSD and MIT licenses (your choice).
130
131
132
133
134David A. Wheeler                    2008-07                           ZENON(1)
Impressum