Summary of the syntax of Expressions:
Summary of the syntax of Formulae:
Boolean operators: ∧, ∨, ¬, ⊃, ≡, ∃V f, ∀V f
∃V f abbreviates ∃V ∈Val f
Syntax of Integer Expressions in BNF:
ie ::= | z |A |ig(ie1,…,ien) |
where z is an integer constant and ig an integer operator.
Syntax of Boolean Expressions in BNF:
be ::= | b |Q |bg(be1,…,ben) |
where b is a Boolean constant and bg an Boolean operator.
Syntax of First Order Formulae in BNF (grammar):
f ::= | true |h(e1,…,en) |¬f | f1 ∧ f2 |∀V f |
where h is a Boolean predicate over integer or Boolean expressions.
Derived formulae:
∃V f | ≜ | ¬∀V ¬f |