Syntax of formulas


Grammar


<phi>, <psi>... ::= bottom | <atomphi> | (<phi> and <psi>) | (<phi> or <psi>) | (not <phi>) | (<phi> imply <psi>) | (<phi> equiv <psi>) | (forall <var> <phi>) | (exists <var> <phi>)

<atomphi> ::= <proposition> | (<predicate> <term> <term> <term> .....)

<term> ::= <constant> | <var> | (<function> <term> <term> <term>....)

<proposition> ::= p, q, etc. (any symbol)
<predicate> ::= p, q etc. (any symbol)
<function> ::= f, g, etc. (any symbol)
<var> ::= x, y, etc. (any symbol)
<constant> ::= s, t, etc. (any symbol)

Example

(p x)
(p x y)
((p x) and (forall x (q x (f x))))