1ZENON-FORMAT(5)                  User Commands                 ZENON-FORMAT(5)
2
3
4

NAME

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

DESCRIPTION

10       Zenon can use several input formats, including its own "Zenon"  format.
11       This document describes this "Zenon" format.
12
13       In  the  Zenon  format, "#" and ";" introduce comments that continue to
14       the end of the line.  Identifiers begin with A-Z, a-z,  or  underscore;
15       they  may  continue  with  0  or  more of the characters A-Z, a-z, 0-9,
16       underscore, and apostrophe.  Strings are enclosed  inside  double-quote
17       characters;  they  may  not contain the double-quote character, control
18       characters, or characters beyond 126.  Whitespace is a token separator,
19       but is otherwise ignored.  Its syntax is as follows:
20              file:
21                | EOF
22                | phrase file
23
24              phrase:
25                | DEF "(" IDENT ident_list ")" expr
26                | HYP int_opt hyp_name expr
27                | GOAL expr
28                | SIG IDENT "(" string_list ")" STRING
29                | INDSET IDENT "(" ident_list ")"
30
31              expr:
32                | IDENT
33                | "(" IDENT expr_list ")"
34                | "(" NOT expr ")"
35                | "(" AND expr expr_list ")"
36                | "(" OR expr expr_list ")"
37                | "(" IMPLY expr expr_list ")"
38                | "(" RIMPLY expr expr_list ")"
39                | "(" EQUIV expr expr_list ")"
40                | "(" TRUE ")"
41                | TRUE
42                | "(" FALSE ")"
43                | FALSE
44                | "(" ALL mlambda ")"
45                | "(" EX mlambda ")"
46                | mlambda
47                | "(" TAU lambda ")"
48                | "(" "=" expr expr ")"
49                | "(" MATCH expr case_list ")"
50                | "(" LET id_expr_list_expr ")"
51
52              expr_list:
53                | expr expr_list
54                | /* empty */
55
56              lambda:
57                | "(" "(" IDENT STRING ")" expr ")"
58                | "(" "(" IDENT ")" expr ")"
59
60              mlambda:
61                | "(" "(" ident_list STRING ")" expr ")"
62                | "(" "(" ident_list ")" expr ")"
63
64              ident_list:
65                | /* empty */
66                | IDENT ident_list
67
68              int_opt:
69                | /* empty */
70                | INT
71
72              hyp_name:
73                | /* empty */
74                | STRING
75
76              string_list:
77                | /* empty */
78                | STRING string_list
79
80              case_list:
81                | /* empty */
82                | "(" IDENT ident_list ")" expr case_list
83
84              id_expr_list_expr:
85                | expr
86                | IDENT expr id_expr_list_expr
87
88
89       With the following token definitions:
90               DEF "$def"
91               GOAL "$goal"
92               HYP "$hyp"
93               INDSET "$indset"
94               INDPROP "$indprop"
95               LET "$let"
96               MATCH "$match"
97               SIG "$sig"
98               NOT "-."
99               AND "/\"
100               OR "\/"
101               IMPLY "=>"
102               RIMPLY "<="
103               EQUIV "<=>"
104               TRUE "T."
105               FALSE "F."
106               ALL "A."
107               EX "E."
108               TAU "t."
109
110

SEE ALSO

112       zenon(1)
113
114

AUTHOR

116       This man page was written by David A. Wheeler.
117

119       Zenon  is  released  under  the  revised BSD license.  This man page is
120       released under both the revised BSD and MIT licenses (your choice).
121
122
123
124
125David A. Wheeler                    2008-07                    ZENON-FORMAT(5)
Impressum