IV.2 Syntax First Order Logic

First Order Logic [Slide 116]

Summary of the syntax of Expressions:

Summary of the syntax of Formulae:

First Order Logic [Slide 117]

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

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