V.5 Syntax First Order ITL

First Order ITL [Slide 156]

Summary of the syntax of Expressions:

Summary of the syntax of Formulae:

First Order ITL [Slide 157]

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.

First Order ITL [Slide 158]

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)

2023-09-12
Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2023