CS 561a: Introduction to Artificial Intelligence
CS 561, Sessions 14-15
75
Resolution
CS 561, Sessions 14-15
76
Resolution inference rule
CS 561, Sessions 14-15
3
Remember: normal forms
“sum of products of
simple variables or
negated simple variables”
“product of sums of
simple variables or
negated simple variables”
77
CS 561, Sessions 14-15
78
Conjunctive normal form – (how-to is coming up…)
CS 561, Sessions 14-15
79
Skolemization
If x has a y we can infer that y exists. However, its existence is contingent on x, thus y is a function of x as H(x).
CS 561, Sessions 14-15
80
Examples: Converting FOL sentences to clause form…
Convert the sentence
1. (x)(P(x) => ((y)(P(y) => P(f(x,y))) ^ ¬(y)(Q(x,y) => P(y))))
(like A => B ^ C)
2. Eliminate =>
(x)(¬P(x) ((y)(¬P(y) P(f(x,y))) ^ ¬(y)(¬Q(x,y) P(y))))
3. Reduce scope of negation
(x)(¬P(x) ((y)(¬P(y) P(f(x,y))) ^ (y)(Q(x,y) ^ ¬P(y))))
4. Standardize variables
(x)(¬P(x) ((y)(¬P(y) P(f(x,y))) ^ (z)(Q(x,z) ^ ¬P(z))))
CS 561, Sessions 14-15
81
Examples: Converting FOL sentences to clause form…
5. Eliminate existential quantification
(x)(¬P(x) ((y)(¬P(y) P(f(x,y))) ^ (Q(x,g(x)) ^ ¬P(g(x)))))
6. Drop universal quantification symbols
(¬P(x) ((¬P(y) P(f(x,y))) ^ (Q(x,g(x)) ^ ¬P(g(x)))))
7. Convert to conjunction of disjunctions
(¬P(x) ¬P(y) P(f(x,y))) ^ (¬P(x) Q(x,g(x))) ^ (¬P(x) ¬P(g(x)))
(x)(¬P(x) ((y)(¬P(y) P(f(x,y))) ^ (z)(Q(x,z) ^ ¬P(z)))) …
CS 561, Sessions 14-15
82
Examples: Converting FOL sentences to clause form…
8. Create separate clauses
¬P(x) ¬P(y) P(f(x,y))
¬P(x) Q(x,g(x))
¬P(x) ¬P(g(x))
9. Standardize variables
¬P(x) ¬P(y) P(f(x,y))
¬P(z) Q(z,g(z))
¬P(w) ¬P(g(w))
(¬P(x) ¬P(y) P(f(x,y))) ^ (¬P(x) Q(x,g(x))) ^ (¬P(x) ¬P(g(x))) …
CS 561, Sessions 14-15
83
Getting back to Resolution proofs …
CS 561, Sessions 14-15
Resolution proof
Want to prove
Note: This is not a
particularly good example
that came from AIMA 1st ed.
AIMA 2nd ed. Ch 9.5 has
much better ones.
84
CS 561, Sessions 14-15
11
Inference in First-Order Logic
Canonical forms for resolution
Conjunctive Normal Form (CNF) Implicative Normal Form (INF)
85
CS 561, Sessions 14-15
12
Example of Refutation Proof
(in conjunctive normal form)
Cats like fish
Cats eat everything they like
Josephine is a cat.
Prove: Josephine eats fish.
cat (x) likes (x,fish)
cat (y) likes (y,z) eats (y,z)
cat (jo)
eats (jo,fish)
86
12
CS 561, Sessions 14-15
86
Refutation
Negation of goal wff: eats(jo, fish)
eats(jo, fish) cat(y) likes(y, z) eats(y, z)
= {y/jo, z/fish}
cat(jo) likes(jo, fish) cat(jo)
=
cat(x) likes(x, fish) likes(jo, fish)
= {x/jo}
cat(jo) cat(jo)
(contradiction)
86
13
CS 561, Sessions 14-15
87
Forward chaining
cat (jo) cat (X) likes (X,fish)
\ /
likes (jo,fish) cat (Y) likes (Y,Z) eats (Y,Z)
\ /
cat (jo) eats (jo,fish) cat (jo)
\ /
eats (jo,fish)
CS 561, Sessions 14-15
88
Backward chaining
Is more problematic and seldom used…
CS 561, Sessions 14-15
89
Example resolution proof
http://www.cs.utexas.edu/~mooney/cs343/slide-handouts/inference.4.pdf
CS 561, Sessions 14-15
90
Example resolution proof
http://www.cs.utexas.edu/~mooney/cs343/slide-handouts/inference.4.pdf
CS 561, Sessions 14-15
91
Example resolution proof
http://www.cs.utexas.edu/~mooney/cs343/slide-handouts/inference.4.pdf
CS 561, Sessions 14-15
19
Example resolution proof
http://www.cs.utexas.edu/~mooney/cs343/slide-handouts/inference.4.pdf
92
CS 561, Sessions 14-15
20
Another example resolution proof
http://www.cs.utsa.edu/~bylander/cs5233/notes/logichandout.pdf
CS 561, Sessions 14-15
21
Another example resolution proof
http://www.cs.utsa.edu/~bylander/cs5233/notes/logichandout.pdf
CS 561, Sessions 14-15
22
Another example resolution proof
http://www.cs.utsa.edu/~bylander/cs5233/notes/logichandout.pdf
…
)
(
)
(
w
Q
w
P
Ú
Ø
)
(
)
(
x
R
x
P
Ú
)
(
)
(
y
S
y
Q
Ú
Ø
)
(
)
(
z
S
z
R
Ú
Ø
)
(
)
(
w
Q
w
P
Þ
)
(
)
(
x
R
x
P
True
Ú
Þ
)
(
)
(
y
S
y
Q
Þ
)
(
)
(
z
S
z
R
Þ
/docProps/thumbnail.jpeg