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