IT3160E

Introduction to Artificial Intelligence

Chapter 4: Knowledge and Inference

Inference in First Order Logic

Lê Thanh Hương
School of Information and Communication Technology - HUST
First Order Logic

• Syntax
• Semantic
• Inference
• Resolution

2
Inference in FOL

• Difficulties
• Quantifiers
• Infinite sets of terms
• Infinite sets of sentences
• Examples: [Link](x)  Greedy(x)  Evil(x)
• Infinite set of instances
King (Bill)  Greedy(Bill)  Evil(Bill)
King (FatherOf (Bill))  Greedy(FatherOf (Bill))  Evil(FatherOf (Bill))
...

3
Robinson’s Resolution

• Herbrand’s Theorem (~1930)

• A set of sentences S is unsatisfiable if and only there exists a finite subset Sg
of the set of all ground instances Gr(S), which is unsatisfiabe
• Herbrand showed that there is a procedure to demonstrate the
unsatisfiability of a unsatisfiable set of sentences
• Robinson propose the Resolution procedure (~1950)

4
Idea of Resolution

• Refutation-based procedure
• S |= A if and only if S {A} is unsatisfible
• Resolution procedure
• Transform S {A} into a set of clauses
• Apply Resolution rule to find a the empty clause (contradiction)
• If the empty clause is found
• Conclude S |= A
• Otherwise
• No conclusion

5
Clause

• A clause is a disjunction of literals, i.e., has the form

P1  P2  ... Pn Pi  []Ri

• Example
P(x)  Q(x, a)  R(b)
P( y)  Q(b, y)  R( y)

• The empty clause corresponds to a contradiction

• Any sentence can be transformed to an equi-satisfiable set of clauses

6
Elements of Resolution

• Resolution rule
• Unification
• Transform a sentence to a set of clauses

7
Resolution rule

• Resolution rule
A B C  D
 = mgu(B, C)
 ( A  D)

• mgu: most general unifier

• The most general assignment of variables to terms in such a way that two terms
are equal
• Syntactical unification algorithm
• : substitution

8
Example of Resolution rule

• x, y are variables
• a, b are constants

P(x)  Q(x, a) Q(b, y)  R( y)

 = {x = b, y = a}
P(b)  R(a)
A  P(x)
B  Q(x, a)
C  Q(b, y)
D  R( y)

9
Example of Resolution rule

10
Elements of Resolution

• Resolution rule
• Unification
• Transform a sentence to a set of clauses

11
Unification

• Input
• Set of equalities between two terms
• Output
• Most general assignment of variables that satisfies all equalities
• Fail if no such assignment exists

12
Unification algorithm

• Vars(U), Vars(t) are sets of variables in U and t

• v is a variable
• s and t are terms
• f and g are function symbols

13
Example of Unification

14
Elements of Resolution

• Resolution rule
• Unification
• Transform a sentence to a set of clauses

15
Transform a sentence to a set of clauses

1. Eliminate implication
2. Move negation inward
3. Standardize variable scope
4. Move quantifiers outward
5. Skolemize existential quantifiers
6. Eliminate universal quantifiers
7. Distribute and, or
8. Flatten and, or
9. Eliminate and

16
Eliminate implication

17
Move negation inward

18
Standardize variable scope

Each variable for each quantifier

19
Move quantifiers outward

20
Existential Instantiation

{ x P(x,a)  (Q(x,b)  R(x,b) }

21
Skolemize existential quantifiers

22
Eliminate universal quantifiers

23
Distribute and, or

24
Flatten and, or

25
Eliminate and

26
Summary of Resolution

• Refutation-based procedure
• S |= A if and only if S {A} is unsatisfiable
• Resolution procedure
• Transform S {A} into a set of clauses
• Apply Resolution rule to find a the empty clause
(contradiction)
• If the empty clause is found
• Conclude S |= A
• Otherwise
• No conclusion

27
Summary of Resolution

• Theorem
• A set of clauses S is unsatisfiable if and only if upon the input S, Resolution
procedure finds the empty clause (after a finite time).

28
Exercice

• The law says that it is a crime for an American to sell weapons to

hostile nations
• The country Nono, an enemy of America, has some missiles, and all
of its missiles were sold to it by Colonel West, who is American
• Is West a criminal?

29
Modeling

The country Nono, an enemy of America,

has some missiles, and all of its missiles
were sold to it by Colonel West, who is
American

30
Example of proof by Resolution

Prove
Criminal(West)

Successful 31
Exercice

• Jack owns a dog own(Jack, dog)

• Every dog owner is an animal lover
• No animal lover kills an animal
• Either Jack or Curiosity killed the cat, who is named Tuna
• Did Curiosity kill the cat?

32
Modeling

Jack owns a dog own(Jack, dog)

Every dog owner is an animal lover
No animal lover kills an animal
Either Jack or Curiosity killed the cat, who is named Tuna
Did Curiosity kill the cat? Kills(Curiosity,Tuna)

[Link](x)  Owns (Jack, x)

xy.(Dog( y)  Owns (x, y))  AnimalLover(x)
xy.(AnimalLover(x)  Animal( y)  Kills(x, y))
Kills(Jack,Tuna)  Kill(Curiosity,Tuna)
Cat (Tuna)
[Link] (x)  Animal(x)

33
Transform the problem to set of clauses

Dog(D)
Owns (Jack, D)
Dog( y)  Owns (x, y)  AnimalLover(x)
AnimalLover(x)  Animal( y)  Kills(x, y)
Kills(Jack,Tuna)  Kill(Curiosity,Tuna)
Cat (Tuna)
Cat (x)  Animal(x)
Kills(Curiosity,Tuna)

34