.TH ZENON-FORMAT "5" "2008-07" "David A. Wheeler" "User Commands" .SH NAME zenon-format \- Automated theorem prover for first-order classical logic format .SH DESCRIPTION .\" Add any additional description here .PP Zenon can use several input formats, including its own "Zenon" format. This document describes this "Zenon" format. .PP 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: .RS 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 .RE .PP With the following token definitions: .RS 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." .RE .SH "SEE ALSO" .PP zenon(1) .SH AUTHOR .PP This man page was written by David A. Wheeler. .SH COPYRIGHT Zenon is released under the revised BSD license. This man page is released under both the revised BSD and MIT licenses (your choice).