L2_First_Order_Logic - AI_for_Beginners, Logic Maths

Logic vị từ

1. Cao Hoang Tru
CSE Faculty - HCMUT
1
09 November 2009
First-Order Logic
• Propositional logic does not represent and cannot 
handle 
objects
. 
• First-order logic is to represent and reason on 
objects
and their 
relations
.
• High-order logic is to deal with 
relations of 
relations
.

2. Cao Hoang Tru
CSE Faculty - HCMUT
2
09 November 2009
First-Order Logic Syntax
•
Constant 
symbols: a, b, c, John, …
to represent
primitive objects
•
Variable 
symbols: x, y, z, …
to represent
unknown objects
•
Predicate
symbols: safe, married, love, …
to represent
relations
married
(John)
love
(John, Mary)

3. Cao Hoang Tru
CSE Faculty - HCMUT
3
09 November 2009
First-Order Logic Syntax
•
Function
symbols: to represent 
simple objects
safe(
square(1, 2)
)
love(
father(John), mother(John)
)
•
Terms
: to represent 
complex objects
– Constant symbols
– If 
f
is a function symbol, and 
t
1
, 
t
2
, …, 
t
n
are terms, 
then so is 
f
(
t
1
, 
t
2
, …, 
t
n
)
love(
mother(father(John))
, John)

4. Cao Hoang Tru
CSE Faculty - HCMUT
4
09 November 2009
First-Order Logic Syntax
• Logical 
connectives
: 
¬
, 
∧
, 
∨
, ⇒, 
⇔
•
Universal quantifier
: 
∀
x: p(x)
∀x love(father(x), mother(x))
•
Existential quantifier
: 
∃
x: p(x) 
≡ ¬∀
x: 
¬
p(x)
∃x 
¬
married(x)

5. Cao Hoang Tru
CSE Faculty - HCMUT
5
09 November 2009
First-Order Logic Syntax
•
Equality
: 
father(John) = Henry
∃x, y brother(x, Richard) ∧brother(y, Richard) ∧ ¬(x = y)

6. Cao Hoang Tru
CSE Faculty - HCMUT
6
09 November 2009
First-Order Logic Syntax
•
Sentences
:
– Atomic sentences: 
p(t
1
, t
2
, …, t
n
)
– If 
α
is a sentence, then so are 
¬α
and 
(
α
)
– If 
α
and 
β
are sentences, then so are 
α ∧β
, 
α ∨β
,           
α 
⇒
β
, and 
α ⇔β
– If 
α
is a sentence, then so are 
∀α
and 
∃α

7. Cao Hoang Tru
CSE Faculty - HCMUT
7
09 November 2009
First-Order Logic Semantics
•
Truth value
with respect to an interpretation 
(possible world)
α
≡∀x: p(f(x), x)

8. Cao Hoang Tru
CSE Faculty - HCMUT
8
09 November 2009
First-Order Logic Semantics
•
Truth value
with respect to an interpretation 
(possible world)
α
≡∀x: p(f(x), x)
•
Possible world
:
– Set of objects
– Constants 
→
objects
– Functions 
→
mapping from objects to objects
– Predicates 
→
relations on objects

9. Cao Hoang Tru
CSE Faculty - HCMUT
9
09 November 2009
First-Order Logic Semantics
α
≡ ∀
x: p(f(x), x)
W
1
:
Set of objects: 
{John, Mary}
Functions: f →
sibling
, sibling(John) = Mary, sibling(Mary) = John
Predicates: p →
love
, {love(John, Mary), love(Mary, John)}
W
2
:
Set of objects: 
{John, Mary}
Functions: f →
sibling
, sibling(John) = Mary, sibling(Mary) = John
Predicates: p →
love
, {love(John, Mary)}
α
is true with respect to 
W
1
, but not 
W
2

10. Cao Hoang Tru
CSE Faculty - HCMUT
10
09 November 2009
FOL: Kinship Domain
∀m, c: mother(c) = m ⇔female(m) ∧parent(m, c)
∀w, h: husband(h, w) ⇔male(h) ∧spouse(h, w)
∀x: male(x) ⇔ ¬female(x)
∀p, c: parent(p, c) ⇔child(c, p)
∀g, c: grand-parent(g, c) ⇔ ∃p: parent(g, p) ∧parent(p, c)
∀x, y: sibling(x, y)  ⇔x ≠y ∧ ∃p: parent(p, x) ∧parent(p, y)

11. Cao Hoang Tru
CSE Faculty - HCMUT
11
09 November 2009
FOL: Number Domain
nat-num(0)
∀n: nat-num(n) ⇒nat-num(succ(n))
∀n: 0 ≠succ(n)
∀m: nat-num(m) ⇒+(0, m) = m
∀m, n: nat-num(m) ∧nat-num(n) ⇒+(succ(m), n) = succ(+(m, n))

12. Cao Hoang Tru
CSE Faculty - HCMUT
12
09 November 2009
FOL: Set Domain
∀s: set(s) ⇔(s = {}) ∨(∃x, s
2
: set(s
2
) ∧s = {x|s
2
})
¬∃x, s: {x|s} = {}
∀x, s: x ∈s ⇔s = {x|s}
∀x, s: x ∈s ⇔ ∃y, s
2
: (s = {y|s
2
} ∧(x = y ∨x ∈s
2
))
∀s
1
, s
2
: s
1
⊆s
2
⇔(∀x: x ∈s
1
⇒x ∈s
2
)
∀s
1
, s
2
: s
1
= s
2
⇔(s
1
⊆s
2
∧s
2
⊆s
1
)

13. Cao Hoang Tru
CSE Faculty - HCMUT
13
09 November 2009
FOL: WumpusGame
•
Environment
:
square(1, 2) ≡[1, 2]
percept([stench, breeze, glitter, none, none], 5)
∀x, y, a, b: adjacent([x, y], [a, b])  ⇔[a, b] ∈{[x+1, y], [x-1, y], 
[x, y+1], [x, y-1]}
∀s, t: at(Agent, s, t)  ∧breeze(t) ⇒breezy(s)
time

14. Cao Hoang Tru
CSE Faculty - HCMUT
14
09 November 2009
FOL: WumpusGame
•
Diagnostic rules
:
∀s: breezy(s) ⇒∃r: adjacent(r, s) ∧pit(r)
∀s: ¬∃r: adjacent(r, s) ∧pit(r) ⇒¬breezy(s) 
∀s: breezy(s) ⇔ ∃r: adjacent(r, s) ∧pit(r)

15. Cao Hoang Tru
CSE Faculty - HCMUT
15
09 November 2009
FOL: WumpusGame
•
Causal rules
:
∀r: pit(r) ⇒(∀s: adjacent(r, s) ⇒breezy(s)) 
∀s: [∀r: adjacent(r, s) ⇒¬pit(r)] ⇒¬breezy(s)

16. Cao Hoang Tru
CSE Faculty - HCMUT
16
09 November 2009
Homework
• In Russell & Norvig’sAIMA (2
nd
ed.): Exercises of 
Chapter 8.

17. Cao Hoang Tru
CSE Faculty - HCMUT
17
09 November 2009
Inference Rules with Quantifiers
•
Substitution
:
SUBST(
θ
, 
α
) = 
α
θ
θ ≡
{x
1
/t
1
, x
2
/t
2
, …, x
n
/t
n
}
SUBST({x/John, y/mother(x)}, love(x, y)) = love(Joh n, mother(John))

18. Cao Hoang Tru
CSE Faculty - HCMUT
18
09 November 2009
Inference Rules with Quantifiers
•
Universal instantiation
: ∀
x: 
α

SUBST({x/ground-term}, 
α
)
∀x: king(x) ∧greedy(x) ⇒evil(x)

king(John) ∧greedy(John) ⇒evil(John)

19. Cao Hoang Tru
CSE Faculty - HCMUT
19
09 November 2009
Inference Rules with Quantifiers
•
Existential instantiation
:
∃
x:
α

SUBST({x/new-constant}, 
α
)
∃x:crown(x) ∧on-head(x, John)

crown(c) ∧on-head(c, John)

20. Cao Hoang Tru
CSE Faculty - HCMUT
20
09 November 2009
Inference Rules with Quantifiers
•
Reduction to propositional inference
:
∀x: king(x) ∧greedy(x) ⇒evil(x) 
king(John)
greedy(John)
king(John) ∧greedy(John) ⇒evil(John)

21. Cao Hoang Tru
CSE Faculty - HCMUT
21
09 November 2009
Inference Rules with Quantifiers
• An offspring of a horse is a horse:
?
• Bluebeard is a horse:
?
• Charlie is Bluebeard’s offspring:
?
• Inferences: horse(Charlie) 
?

22. Cao Hoang Tru
CSE Faculty - HCMUT
22
09 November 2009
Inference Rules with Quantifiers
• An offspring of a horse is a horse:
∀x, y: horse(x) ∧offspring(x, y) ⇒horse(y)
• Bluebeard is a horse:
horse(Bluebeard)
• Charlie is Bluebeard’s offspring:
offspring(Bluebeard, Charlie)
• Inference: 
horse(Charlie)

23. Cao Hoang Tru
CSE Faculty - HCMUT
23
09 November 2009
Generalized Modus Ponens
p
1
’, p
2
’, …, p
n
’, (p
1
, p
2
, …, p
n
⇒q)

SUBST(
θ
, q)
p
i 
and p’
i
are atomic
SUBST(θ, p
i) = SUBST(θ, p
i’) 

24. Cao Hoang Tru
CSE Faculty - HCMUT
24
09 November 2009
Generalized Modus Ponens
•
Unification
:
UNIFY(p, q) = 
θ
where SUBST(θ, p) = SUBST(θ, q)
knows(John, x) ⇒hates(John, x)
knows(John, Jane)
knows(x, Leonid)
knows(x, mother(Y))
knows(x, Elizabeth)
UNIFY(knows(John, x), knows(John, Jane)) = {x/Jane}
UNIFY(knows(John, x), knows(y, Leonid)) = {x/Leonid, y/John}
UNIFY(knows(John, x), knows(y, mother(y))) = {y/John, x/mother(John)}
UNIFY(knows(John, x), knows(x, Elizabeth)) =
fail

25. Cao Hoang Tru
CSE Faculty - HCMUT
25
09 November 2009
Generalized Modus Ponens
•
Standardization
:
UNIFY(knows(John, x
1
), knows(x
2
, Elizabeth)) = {x
1
/John, x
2
/Elizabeth}

26. Cao Hoang Tru
CSE Faculty - HCMUT
26
09 November 2009
Generalized Modus Ponens
•
Most generalized unifier
:
UNIFY(knows(John, x), knows(y, z)) 
= {y/John, x/John, z/John}
= {y/John, x/Jane, z/Jane}
= {y/John, x/v, z/v}
= {y/John, x/z, v/Jane}
= 
{y/John, x/z}

27. Cao Hoang Tru
CSE Faculty - HCMUT
27
09 November 2009
Forward Chaining
• An offspring of a horse is a horse:
?
• Bluebeard is a horse:
?
• Bluebeard is Charlie’s parent:
?
• Offspring and parent are inverse relations: 
?

28. Cao Hoang Tru
CSE Faculty - HCMUT
28
09 November 2009
Forward Chaining
• An offspring of a horse is a horse:
∀x,y horse(x) ∧∧∧∧offspring(x, y) ⇒horse(y)
• Bluebeard is a horse:
horse(Bluebeard)
• Bluebeard is Charlie’s parent:
parent(Charlie, Bluebeard)
• Offspring and parent are inverse relations: 
∀x,y offspring(x, y) ⇔parent(y, x)

29. Cao Hoang Tru
CSE Faculty - HCMUT
29
09 November 2009
Backward Chaining
horse(z)
{z/Bluebeard}
horse(z)
horse(Bluebeard)
offspring(Bluebeard, z)
{z/Charlie}
parent(z, Bluebeard)
∀x,y horse(x) ∧offspring(x, y) ⇒horse(y)
horse(Bluebeard)
parent(Charlie, Bluebeard)

30. Cao Hoang Tru
CSE Faculty - HCMUT
30
09 November 2009
Generalized Resolution
p
1 
∨
…
p
j
…
∨
p
m
q
1 
∨
…
q
k
…
∨
q
n

resolvent: SUBST(
θ
, p
1 
∨
… p
j-1 
∨
p
j+1 
…
∨
p
m
∨
q
1 
∨
… q
k-1 
∨
q
k+1 
…
∨
q
n
)
UNIFY(p
j
, ¬q
k
) = θfor literals p
j
and q
k

31. Cao Hoang Tru
CSE Faculty - HCMUT
31
09 November 2009
Generalized Resolution
• Conjunctive normal form
:
∀x: p(x) ⇒q(x)
∀x: ¬p(x) ⇒r(x)
∀x: q(x) ⇒s(x)
∀x: r(x) ⇒s(x)
¬p(x) ∨∨∨∨q(x)
p(y) ∨∨∨∨r(y)
¬q(z) ∨∨∨∨s(z)
¬r(t) ∨∨∨∨s(t)

32. Cao Hoang Tru
CSE Faculty - HCMUT
32
09 November 2009
Generalized Resolution
• Refutation proof procedure:
KB
|=|=|= |= α
if and only if 
KB 
∧∧∧∧¬¬¬¬α |=|=|= |=
false

33. Cao Hoang Tru
CSE Faculty - HCMUT
33
09 November 2009
Generalized Resolution
• Conjunctive normal form
:
∀x: p(x) ⇒q(x)
∀x: ¬p(x) ⇒r(x)
∀x: q(x) ⇒s(x)
∀x: r(x) ⇒s(x)
¬p(x) ∨∨∨∨q(x)
p(y) ∨∨∨∨r(y)
¬q(z) ∨∨∨∨s(z)
¬r(t) ∨∨∨∨s(t)
|= |= |=  |= s(a)

34. Cao Hoang Tru
CSE Faculty - HCMUT
34
09 November 2009
Generalized Resolution
¬p(x) ∨∨∨∨q(x)
¬p(x) ∨∨∨∨q(x)
p(y) ∨∨∨∨r(y)
¬q(z) ∨∨∨∨s(z)
¬r(t) ∨∨∨∨s(t)
¬q(z) ∨∨∨∨s(z)
¬p(z) ∨∨∨∨s(z)
p(y) ∨∨∨∨r(y)
s(y) ∨∨∨∨r(y)
¬r(t) ∨∨∨∨s(t)
s(t)
¬s(a)

35. Cao Hoang Tru
CSE Faculty - HCMUT
35
09 November 2009
Generalized Resolution
• Refutation proof procedure:
sound
and
complete

36. Cao Hoang Tru
CSE Faculty - HCMUT
36
09 November 2009
Generalized Resolution
• Conversion to CNF:
– Eliminate implications: 
p ⇒q ≡ ¬p ∨∨∨∨q
– Move 
¬
inwards: ¬(p ∨∨∨∨q) ≡ ¬p ∧∧∧∧ ¬q
¬(p ∧∧∧∧q) ≡ ¬p ∨∨∨∨ ¬q
¬∀x p≡ ∃x ¬p
¬∃x p≡ ∀x ¬p
¬¬p≡p
– Standardize variables: 
(∀x p(x))∨∨∨∨(∃x p(x))≡(∀x p(x))∨∨∨∨(∃y q(y))

37. Cao Hoang Tru
CSE Faculty - HCMUT
37
09 November 2009
Generalized Resolution
• Conversion to CNF (cont.):
– Move quantifiers left: 
p ∨∨∨∨q ≡ ∀X p ∨∨∨∨q
– Skolemize (to remove 
∃
):
∃x p(x)≡p(c)
Skolem constant
∀x ∃y p(x, y)≡ ∀x p(x, f(x))
Skolem function
– Distribute 
∧∧∧∧
over 
∨∨∨∨
: 
(p ∧∧∧∧q)∨∨∨∨r ≡(p ∨∨∨∨r) ∧∧∧∧(q ∨∨∨∨r)
– Flatten nested conjunctions and disjunctions: 
(p ∨∨∨∨q)∨∨∨∨r ≡(p ∨∨∨∨q ∨∨∨∨r)
(p ∧∧∧∧q)∧∧∧∧r ≡(p ∧∧∧∧q ∧∧∧∧r)

38. Cao Hoang Tru
CSE Faculty - HCMUT
38
09 November 2009
Generalized Resolution
• Jack owns a dog:
?
• Every dog owner is an animal lover:
?
• No animal lover kills an animal:
?
• Either Jack or Fred killed cat Kiko:
?

39. Cao Hoang Tru
CSE Faculty - HCMUT
39
09 November 2009
Generalized Resolution
• Jack owns a dog:
∃x: dog(x) ∧∧∧∧own(Jack, x)
• Every dog owner is an animal lover:
∀x: (∃y dog(y) ∧∧∧∧own(x, y)) ⇒animal-loverx)
• No animal lover kills an animal:
∀x: animal-lover(x)⇒∀y animal(y)⇒¬kill(x, y)
• Either Jack or Fred killed cat Kiko:
kill(Jack, Tuna) ∨∨∨∨kill(Fred, Kiko)

40. Cao Hoang Tru
CSE Faculty - HCMUT
40
09 November 2009
Generalized Resolution
dog(c) 
owns(Jack, c)
¬dog(y) ∨∨∨∨ ¬own(x, y) ∨∨∨∨animal-lover(x)
¬animal-lover(x)∨∨∨∨ ¬animal(y)∨∨∨∨ ¬kill(x, y)
kill(Jack, Kiko) ∨∨∨∨kill(Fred, Kiko)
cat(Kiko)
¬cat(x) ∨∨∨∨animal(x)
⇒kill(Fred, Kiko)

41. Cao Hoang Tru
CSE Faculty - HCMUT
41
09 November 2009
Logic Programming
• Robinson, J.A. 1965. 
A machine-oriented logic based on 
the resolution principle
. Journal of ACM 12 (1): 23-41.
• Kowalski, R.A. & Kuehner, D. 1971. 
Linear Resolution with 
Selection Function
. Artificial Intelligence 2 (3/4): 227-260.
• Kowalski, R.A. 1979. 
Algorithm = Logic + Control
. 
Communication of ACM 22 (7): 424-436.
• Lloyd, J.W. 1987. 
Foundations of Logic Programming
(2
nd
ed.). 

42. Cao Hoang Tru
CSE Faculty - HCMUT
42
09 November 2009
Logic Programming
• Definite logic program:
A ←B
1
, B
2
, …, B
m
≡A ∨∨∨∨ ¬B
1 
∨∨∨∨ ¬B
2
∨∨∨∨…∨∨∨∨ ¬B
m
(
program clause
)
head body ←A
1
, A
2
, …, A
n  
≡ ¬A
1 
∨∨∨∨ ¬A
2
∨∨∨∨…∨∨∨∨ ¬A
n    
(
goal clause
)
A, B
i, A
j: 
atoms

43. Cao Hoang Tru
CSE Faculty - HCMUT
43
09 November 2009
Logic Programming
•
PROLOG
(Alain Colmerauer 1972): allowing only Horn 
clauses (definite clauses)

44. Cao Hoang Tru
CSE Faculty - HCMUT
44
09 November 2009
Logic Programming
• The occur-check is omitted from the unification 
⇒
unsound
test ←p(x, x)
p(x, f(x))

45. Cao Hoang Tru
CSE Faculty - HCMUT
45
09 November 2009
Logic Programming
• Backward chaining with depth-first search         
⇒
incomplete
p(x, y) ←q(x, y)
q(x, y) ←q(y, x)
p(x, x)

46. Cao Hoang Tru
CSE Faculty - HCMUT
46
09 November 2009
Logic Programming
• Unsafe cut ⇒
incomplete
A ←B, C←A
B ←D, 
!
, E
D ← ←B, C
←D, 
!
, E, C
←
!
, E, C

47. Cao Hoang Tru
CSE Faculty - HCMUT
47
09 November 2009
Logic Programming
•
Negation as failure
: 
conclude 
¬
P if fails to prove P
(closed-world assumption)

48. Cao Hoang Tru
CSE Faculty - HCMUT
48
09 November 2009
Exercises
• In Russell & Norvig’sAIMA (2
nd
ed.): Exercises of 
Chapter 9.