zenon-format - Man Page

Automated theorem prover for first-order classical logic format

Description

Zenon can use several input formats, including its own "Zenon" format. This document describes this "Zenon" format.

In the Zenon format, "#" and ";" introduce comments that continue to the end of the line. Identifiers begin with A-Z, a-z, or underscore; they may continue with 0 or more of the characters A-Z, a-z, 0-9, underscore, and apostrophe. Strings are enclosed inside double-quote characters; they may not contain the double-quote character, control characters, or characters beyond 126. Whitespace is a token separator, but is otherwise ignored. Its syntax is as follows:

file:
 | EOF
 | phrase file

phrase:
 | DEF "(" IDENT ident_list ")" expr
 | HYP int_opt hyp_name expr
 | GOAL expr
 | SIG IDENT "(" string_list ")" STRING
 | INDSET IDENT "(" ident_list ")"

expr:
 | IDENT
 | "(" IDENT expr_list ")"
 | "(" NOT expr ")"
 | "(" AND expr expr_list ")"
 | "(" OR expr expr_list ")"
 | "(" IMPLY expr expr_list ")"
 | "(" RIMPLY expr expr_list ")"
 | "(" EQUIV expr expr_list ")"
 | "(" TRUE ")"
 | TRUE
 | "(" FALSE ")"
 | FALSE
 | "(" ALL mlambda ")"
 | "(" EX mlambda ")"
 | mlambda
 | "(" TAU lambda ")"
 | "(" "=" expr expr ")"
 | "(" MATCH expr case_list ")"
 | "(" LET id_expr_list_expr ")"

expr_list:
 | expr expr_list
 | /* empty */

lambda:
 | "(" "(" IDENT STRING ")" expr ")"
 | "(" "(" IDENT ")" expr ")"

mlambda:
 | "(" "(" ident_list STRING ")" expr ")"
 | "(" "(" ident_list ")" expr ")"

ident_list:
 | /* empty */
 | IDENT ident_list

int_opt:
 | /* empty */
 | INT

hyp_name:
 | /* empty */
 | STRING

string_list:
 | /* empty */
 | STRING string_list

case_list:
 | /* empty */
 | "(" IDENT ident_list ")" expr case_list

id_expr_list_expr:
 | expr
 | IDENT expr id_expr_list_expr

With the following token definitions:

DEF "$def"
GOAL "$goal"
HYP "$hyp"
INDSET "$indset"
INDPROP "$indprop"
LET "$let"
MATCH "$match"
SIG "$sig"
NOT "-."
AND "/\"
OR "\/"
IMPLY "=>"
RIMPLY "<="
EQUIV "<=>"
TRUE "T."
FALSE "F."
ALL "A."
EX "E."
TAU "t."

See Also

zenon(1)

Author

This man page was written by David A. Wheeler.

Referenced By

zenon(1).

2008-07 David A. Wheeler