Logics for Data and Knowledge
Representation
Exercises: First Order Logics (FOL)
Originally by Alessandro Agostini and Fausto Giunchiglia
Modified by Fausto Giunchiglia, Rui Zhang and Vincenzo Maltese
Logical Modeling
Language
L
I
Realization
Domain
D
SEMANTIC
GAP
2
Mental
Model
Meaning
Theory
T
⊨
Entailment
World
Interpretation
Modeling
Data
Knowledge
Model
M
The need for greater expressive power

3
We need FOL for a greater expressive power. In FOL we have:
 constants/individuals (e.g. 2)
 variables (e.g. x)
 Unary predicates (e.g. Man)
 N-ary predicates (eg. Near)
 functions (e.g. Sum, Exp)
 quantifiers (∀, ∃)
 equality symbol = (optional)
Syntax
4
Alphabet of symbols in FOL






Variables
Constants
Predicate symbols
Function symbols
x1, x2, …, y, z
a1, a2, …, b, c
A11, A12, …, Anm
f11, f12, …, fnm
Logical symbols
Auxiliary symbols
∧, ∨, ,  , ∀, ∃
()

Indexes on top are used to denote the number of arguments, called arity, in
predicates and functions.

Indexes on the bottom are used to disambiguate between symbols having
the same name.

Predicates of arity =1 correspond to properties or concepts
5
Terms

Terms can be defined using the following BNF grammar:
<term> ::= <variable> | <constant> | <function> (<term> {,<term>}*)
x, 2, SQRT(x), Sum(2, 3), Sum(2, x), Average(x1, x2, x3)

A term is called a closed term iff it does not contain variables
Sum(2, 3)
6
Well formed formulas

Well formed formulas (wff) can be defined in BNF as follows:
<atomic formula> ::= <predicate> (<term> {,<term>}*) | <term> = <term>
<wff> ::= <atomic formula> | ¬<wff> | <wff> ∧ <wff> | <wff> ∨ <wff> |
<wff>  <wff> | ∀ <variable> <wff> | ∃ <variable> <wff>
Man(x)
Odd(3)
∀x (Odd(x)  Even(x))
∃x (Dog(x)  White(x))
∃x ∃y (Dog(x)  Dog(y)  (x = y))
∀x (Even(x)  GreaterThan(x,2)  ∃y∃z (Prime(y)  Prime(z)  x = Sum(y,z)))
NOTE: We can also write ∃x.P(x) or ∃x:P(x) as notation (with ‘.’ or “:”)
7
Write in FOL the following NL sentences

“Einstein is a scientist”
Scientist(einstein)

“There is a monkey”
∃x Monkey(x)

“There exists a dog which is black”
∃x (Dog(x)  Black(x))

8
“All persons have a name”
∀x (Person(x)  ∃y Name(x, y))
Write in FOL the following NL sentences

“The sum of two odd numbers is even”
∀x ∀y ( Odd(x)  Odd(y)  Even(Sum(x,y)) )

“A father is a male person having at least one child”
∀x ( Father(x)  Person(x)  Male(x)  ∃y hasChilden(x, y) )

“There is exactly one dog”
∃x Dog(x)  ∀x ∀y ( Dog(x)  Dog(y)  x = y )

“There are at least two dogs”
∃x ∃y ( Dog(x)  Dog(y)  (x = y) )
9
The use of FOL in mathematics

Express in FOL the fact that every natural number x multiplied by 1
returns x (identity):
∀x ( Natural(x)  (Mult(x, 1) = x) )

Express in FOL the fact that the multiplication of two natural
numbers is commutative:
∀x ∀y ( Natural(x)  Natural(y)  (Mult(x, y) = Mult(y, x)) )
10
The use of FOL in mathematics

FOL has being introduced to express mathematical properties

The set of axioms describing the properties of equality between
natural numbers (by Peano):
Axioms about equality
1.
∀x1 (x1 = x1)
reflexivity
2.
∀x1 ∀x2 (x1 = x2  x2 = x1)
symmetricity
3.
∀x1 ∀x2 ∀x3 (x1 = x2  x2 = x3  x1 = x3)
transitivity
4.
∀x1 ∀x2 (x1 = x2  S(x1) = S(x2))
successor
NOTE: Other axioms can be given for the properties of the successor, the
addition (+) and the multiplication (x).
11
Modeling the club of married problem
There are exactly three people in the club, Tom, Sue and
Mary. Tom and Sue are married. If a member of the club is
married, their spouse is also in the club. Mary is not
married.
L = {tom, sue, mary, Club, Married}
Club(tom)  Club(sue)  Club(mary)  ∀x (Club(x)  (x = tom  x = sue  x = mary))
Married(tom, sue)
∀x ∀y ((Club(x)  Married(x, y))  Club(y))
 ∃x Married(mary, x)
12
Modeling the club of married problem (II)
There are exactly three people in the club, Tom, Sue and
Mary. Tom and Sue are married. If a member of the club is
married, their spouse is also in the club.
Add enough common sense FOL statements (e.g.
everyone has at most one spouse, nobody can be married
to himself or herself, Tom, Sue and Mary are different
people) to make it entail that Mary is not married in FOL.
L = {tom, sue, mary, Club, Married}
S1: Club(tom)  Club(sue)  Club(mary)  ∀x (Club(x)  (x = tom  x = sue  x = mary))
S2: Married(tom, sue)
S3: ∀x ∀y ((Club(x)  Married(x, y))  Club(y))
S4:  ∃x Married(mary, x)
13
Modeling the club of married problem (III)
There are exactly three people in the club, Tom, Sue and
Mary. Tom and Sue are married. If a member of the club is
married, their spouse is also in the club.
Add enough common sense FOL statements (e.g.
everyone has at most one spouse, nobody can be married
to himself or herself, Tom, Sue and Mary are different
people) to make it entail that Mary is not married in FOL.
We need to add the following:
S5: ∀x ∀y ((Married(x, y)  Married(y, x))
simmetry
S6: ∀x ∀y ∀z ((Married(x, y)  Married(x, z)  y = z)
at most one wife
S7:  ∃x Married(x, x)
nobody is married with
himself/herself
S8:  (tom=sue)   (tom=mary)   (mary=sue)
14
unique name assumption
Analogy with Databases
EMPLOYEE
NAME
POSITION
MANAGER
Enzo
PhD
Fausto
Fausto
Professor
Bassi
Feroz
PhD
Enzo
“List name, position and manager of the employees”
γ = Employee(x, y, z)
Qγ = All the tuples in the Relation
“List managers of the employees named Enzo”
γ = ∃y Employee(Enzo, y, z)
Qγ = {(Fausto)}
15
SELECT
EMPLOYEE
NAME
POSITION
MANAGER
Enzo
PhD
Fausto
Fausto
Professor
Bassi
Feroz
PhD
Enzo
“List name and position of the employees having a manager”
γ = ∃z Employee(x, y, z)
Qγ = {(Enzo, PhD), (Fausto, Professor), (Feroz, PhD)}
16
FILTER
EMPLOYEE
NAME
POSITION
MANAGER
AGE
Enzo
PhD
Fausto
35
Fausto
Professor
Bassi
40
Feroz
PhD
Enzo
20
“List name and position of the employees with Fausto as manager”
γ = ∃z Employee(x, y, Fausto, z)
Qγ = {(Enzo, PhD)}
“List name and position of the employees with age > 28”
γ = ∃w ∃z (Employee(x, y, z, w) ∧ (w > 28))
Qγ = {(Enzo, PhD), (Fausto, Professor)}
17
JOIN
FACULTY
DEPT
NAME
POSITION
MANAGER
NAME
DEPT
Enzo
PhD
Fausto
Enzo
DISI
Fausto
Professor
Bassi
Fausto
DISI
Feroz
PhD
Enzo
Feroz
MATH
“List name of faculty members and their department”
γ = ∃y ∃z ( Faculty(x, y, z) ∧ Dept(x, w) )
Qγ = {(Enzo, DISI), (Fausto, DISI), (Feroz, MATH)}
“List name of faculty members who belong to all departments”
γ = ∀w (∃x Dept(x, w)  ∃y ∃z (Faculty(x, y, z) ∧ Dept(x, w)))
18
Semantics
19
Interpretation
20
Example of Interpretation
∆ = {tom, sue, mary, club, married, age, sum}
CLUB
Tom
Constants:
I(tom) = Tom, I(sue) = Sue, I(mary) = Mary
Sue
Mary
MARRIED
Unary predicates:
Tom
Sue
Club(tom), Club(sue), Club(Mary)
Robert
Mary
Binary predicates:
Married(tom, sue)
∆1
age
Tom
∆
40
Sue
35
Mary
18
Functions:
∆2
age(tom) = 40, age(sue) = 35, age(mary) =18
sum(3, 5) = 8
21
3
sum
5
∆
8
Interpretation of terms
22
Interpretation of terms
Constants
I(tom)[a] = I(tom) = Tom
I(sue)[a] = I(sue) = Sue
Variables
I(x) [a] = a(x) = tom
I(y) [a] = a(y) = sue
I(z) [a] = a(z) = 3
Functions
I(age(x))) [a] = I(age) (I(x)[a]) = age(a(x)) = age(tom) = 40
I(sum(z, 5))[a] = I(sum) I(I(z)[a], I(5)[a]) = sum(a(z), 5) = sum(3,5) = 8
23
Satisfiability of a formula
24
Satisfiability of simple formulas (I)
Satisfiability is given w.r.t an assignment a.Verify the following:
I ⊨ tom = sue [a]
verify whether: I(tom) [a] = I(sue) [a]
I ⊨ Married(tom, sue) [a]
verify whether: <I(tom) [a], I(sue) [a]>  Married
I ⊨ Married(tom, y) [a]
verify whether: <I(tom) [a], I(y) [a]>  Married
I ⊨  Married(tom, y) [a]
verify whether: <I(tom) [a], I(y) [a]>  Married
I ⊨ ∃x Married(mary, x) [a]
verify whether there exist any d such that
I ⊨ ∀x Married(mary, x) [a]
<Mary, d>  Married
verify whether for all d <Mary, d>  Married
25
Satisfiability of simple formulas (II)

∆ = {0, 1, 2, 3}
constants = {zero}
variables = {x}
predicate symbols = {even, odd}
functions = {succ}
γ1 : ∀x (even(x)  odd(succ(x)))
γ2 : even(zero)
γ3 : odd(zero)
Is there any I and a such that I ⊨ γ1  γ2 [a]?
I(zero)[a] = I(zero) = 0
I(succ(x))[a] = I(succ)(I(x)[a]) = S(n) = {0 if n=3, n+1 otherwise}
I(even) = {0, 2}
I(odd) = {1, 3}
Is there any I and a such that I ⊨ γ1  γ3 [a]?
Yes! Just invert the interpretation of even and odd.
26
Modeling “blocks world”
27
Satisfiability of the problem of blocks

Express the following problem in FOL: “There are 3 blocks A,
B, C in a stack. Each block can be either black or white. We know that
the block A is on the bottom. A block is on the top if there are no blocks
above it. It is possible to be on top if and only if the block is black”.

Constants = {a, b, c}

Predicates = {Black, White, Top}

Relations = {Above}
γ1 : ∃x Above(a,x)
γ2 : Top(y)  Black(y)  ∃z Above(z,y)
28
C
B
A
Satisfiability of the problem of blocks (II)

Constants = {a, b, c}

Predicates = {Black, White, Top}

Relations = {Above}
C
B
A
γ1 : ∃x Above(a,x)
γ2 : Top(y)  Black(y)  ∃z Above(z,y)

Is Γ = {γ1, γ2} satisfiable? Is there any I and an assignment a such that
I ⊨ γ1 [a] and I ⊨ γ2 [a]?
∆ = {A, B, C}
I(a) = A I(b) = B I(c) = C I(Black) = {A, C}
I(Top) = {C} I(Above) = {<B,A>, <C,B>}
I(y)[a] = a(y) = C
I(White) = {B}
NOTE: we can assign a different color to A and B. y is free.
29
Entailment (logical consequence)


Given:
α : ∀x ∀y ∃z (p(x, y)  (p(x, z)  p(z, y)))
β : ∀x ∀y (p(x, y)  ∃z (p(x, z)  p(z, y)))
Does α ⊨ β?
Yes, because in α we can put ∃z inside:
∀x ∀y (∃z p(x, y)  ∃z (p(x, z)  p(z, y)))
z is not in the scope of ∃z p(x, y) and therefore we obtain β
30
Entailment (logical consequence)

For all formulas of the form p(x, y):
1. Is ∃x∃y p(x, y) ⊨ ∃y∃x p(x, y)?
2. Is ∃x∀y p(x, y) ⊨ ∀y∃x p(x, y)?
3. Is ∀x∃y p(x, y) ⊨ ∃y∀x p(x, y)?
If no provide a counterexample.
Assume p(x, y) is x  y.
(1) Yes. The two formulas both says that there are at least two objects which
are related via p.
(2) Yes. The first formula says that there is an x such that for all y we have x
 y. We can take x = 0. The second formula says that for all y there exist an
x such that x  y. x = 0 is fine again.
(3) In this case is No. The first formula says that for all x there exist a y such
that x  y. We can take y = Succ(x). The second formula says that there
exists a y such that for all x we have x  y. We should take y = +.
31
Reasoning
32
Model checking
33
How to prove validity in finite domains

Is it possible to prove that:
⊨ ∀x (Person(x)  Male(x)) [a] where D = {a, b, c}
We have only 3 possible assignments a(x) = a, a(x) = b, a(x) = c
We can translate it as follows:
P: (Person(a)  Male(a))  (Person(b)  Male(b))  (Person(c)  Male(c))
P: (Person(a)  Male(a))  (Person(b)  Male(b))  (Person(c)  Male(c))
P: (Person-a  Male-a)  (Person-b  Male-b)  (Person-c  Male-c)
We check that DPLL(P) returns false.
34