ITL
© 1996-2015







14 Syntax First Order Logic

Syntax of Integer Expressions:

  • Integer values: 0,1,... ,
  • Static integer variable: a,b,...
  • State integer variable: A, B,...
  • Integer operators: +, - ,*,**, mod,div,...

Syntax of Formulae:

  • Boolean values: true,false
  • Boolean predicates: e1 = e2,e1 ⁄= e2,e1 < e2,e1 ≤ e2, e1 > e2,e1 ≥ e2,...
  • Boolean operators: ∧,∨,, ⊃, ≡ , ∀v  o f (for all v such that f holds)

Syntax of Integer Expressions in BNF:

e ::=   z|a|A|g(e1,...,en)

where z is an integer constant and g an integer operator.

Syntax of First Order Formulae in BNF:

f ::=  true|q|Q| h(e1,...,en)|f |f1 ∧ f2|∀v o f

where h is a Boolean predicate.

Derived formulae:

∃v o f =^  ∀v  o f