Prover9/Mace4 BNF
David A. Wheeler, 2007-09-21
The following attempts to document prover9's syntax for formulas, in BNF
format. Note that symbols can be changed and added, including whether they are
prefix, infix, and so on; this BNF only describes the default.
A formulas(sos), formulas(assumptions), and formulas(goals) contains
a list of zero or more "top_level_formula"s. This is based on the
Aug 2007 version of prover9. There may be errors.
A "formula" is essentially the 'type' of a built-in boolean, while
"term" is essentially the 'type' of everything else.
top_level_formula ::= formula "."
formula ::= formula binary_operation formula | "-" formula |
quantifier variable formula | "(" formula ")" |
predicate | term equality_related_ops term |
"$T" | "$F" |
formula "#" attribute
equality_related_ops ::= "=" | "!="
binary_operation ::= "|" | "&" | "->" | "<-" | "<->"
quantifier ::= "all" | "exists"
predicate ::= predicate_name "(" term { "," term }* ")"
term ::= function_name { "(" term { "," term }* ")" } |
term binary_term_operation term |
prefix_term_operation term |
term postfix_term_operation | list
binary_term_operation ::= "==" | "<" | "<=" | ">" | ">=" |
"+" | "*" | "@" | "/" | "\" | "^" | "v"
% Note: Lacks infix "-".
prefix_term_operation ::= "-"
% Note that prefix "-" can form either a formula or a term.
postfix_term_operation ::= "'"
list ::= "[]" |
"[" term { "," term}* [":" term] "]"
% list notation is shorthand for $cons(...).
attribute ::= "label" "(" string ")" |
"answer" "(" term ")" |
"action" "(" term ")"
"bsub_hint_wt" "(" integer ")"