Transcript Knowledge4

We have seen that we can use Generalized Modus Ponens
(GMP) combined with search to see if a fact is entailed from a
Knowledge Base.
Unfortunately, there are some facts that we cannot prove using GMP
Suppose we have in our KB
GoToSchool(Joe)  GoToSchool(Sue)
GoToSchool(Joe)  GoToSchool(Sue)
And we want to know if
GoToSchool(Sue)
Although humans can look at such a KB and immediately see that
GoToSchool(Sue) is true, GMP cannot entail that fact!!
So GMP is not complete.
Is there any complete inference
procedure for FOL?
Yes! It is called resolution refutation (or just resolution).
• It is complete.
• It is sound.
• It is optimally efficient.
• It works for KB in any format unlike GMP which only works
for KBs in Horn clause format (although we generally have to reorganize the format).
Suppose you know that you are going to fail or pass CS 170. Further,
since this is the only class you need to graduate, you know that you are
going to either not pass the class or graduate on time.
Then you can derive the fact that you will either not pass or you graduate
on time.
Fail or Pass, not Pass or GraduateOnTime
Therefore Fail or GraduateOnTime
F
P
G
Fail
Pass
Graduate on time
F  P,
P  G
FG
An intuitive look at why resolution works.
A
B
A
A  B
AB
True
True
False
True
True
True
False
False
False
False
False
True
True
True
True
False
False
True
True
True
In general we know that A  B is equivalent
to A  B
So I could rewrite
A  B, B  C |- A  C as
A  B, B  C
(A)  B, B  C
(A)  B, B  C
A  B, B  C
||||-
AC
AC
A  C
A  C
This is very intuitive! If not A implies B, and B implies C, then
surely A also implies C.
Not raining implies sunny, sunny implies go to the beach, therefore not raining
implies go to the beach.
How resolution refutation works I
Suppose our KB consists the following sentences
PQ
P  R
Q  R
And the goal is to prove R  S
We negate the goal, so R  S becomes (R  S)
R  S
R , S
Now we add R , S to our knowledge base
and look for a contradiction.
(by De Morgan’s law)
(And-Elimination)
PQ
P  R
Q  R
R
S
PQ
P  R
Q  R
R
S
How resolution refutation works II
PQ
QP
P  R
QR
Q  R
R
R
R R Contradiction!
That's all there is to resolution for propositional logic, for first order logic we
just have to put the KB in the right format, otherwise it works the same.
In order for resolution to work for FOL, the KB must be in Conjunctive Normal Form (CNF)
Conjunctive Normal Form: The KB is a conjunction of disjunctions
P(w)  Q(w)
P(x)  R(x)
Q(y)  S(y)
R(z)  S(z)
The Goal is S(A),
so negate it and add
it to the KB
P(w)  Q(w)
SUBST{y/w}
P(w)  S(w)
S(w)  P(w)
P(x)  R(x)
SUBST{w/x}
P(w)  Q(w)
P(x)  R(x)
Q(y)  S(y)
R(z)  S(z)
S(A)
Now lets look for a
contradiction…
Q(y)  S(y)
R(z)  S(z)
S(x)  R(x)
SUBST{x/A, z/A}
S(A)
We will address the problem of
translating an arbitrary KB into
CNF in the next few slides.
Contradiction!
S(A)
S(A)  S(A)
We have seen that we can do resolution when the KB is in CNF.
But most KB are not is that format.
Theorem: We can convert any KB to CNF
• Eliminate Implications
• Move  inwards
• Standardize Variables
• Move Quantifiers left
• Skolemize {Eliminate Existential Quantifiers, Drop Universal Quantifiers }
• Distribute  over 
• Flatten nested conjunctions and disjunctions.
Note that we must do the steps in order!
Eliminate Implications
Change all implication sentences to disjunctions
So
AB
becomes
C  D becomes
etc
A  B
C  D
Move  inwards
Negation is only allow on atom, not whole sentences.
So
(A  B) becomes
A  B
A  B
(A  B)
becomes
x P
x P
becomes
becomes
x P
P
becomes
P
x P
Standardize Variables
Make sure that you are not using the same variable name twice in
a single sentence (unless you really meant to).
So
( x P(x) )  ( x Q(x) )
becomes
( x P(x) )  ( z Q(z) )
Move Quantifiers left
Move all quantifiers left, but keep them in order!
So
x P(x)  y Q(y)
becomes
x y P(x)  Q(y)
Skolemize {Eliminate Existential Quantifiers, Drop Universal Quantifiers }
Existential quantifiers can be eliminated by the introduction of a new
constant that does not appear elsewhere in the database.
x P(x)  Q(x) becomes
P(A)  Q(A)
SUBST{x/A}
One possible complication occurs if we also have Universal quantifiers… Consider
x
person(x)  y heart(y)  has(x,y)
Becomes by
x
SUBST{y/H}
person(x)  heart(H)  has(x,H)
!!!
Instead we have to create a new (Skolem) function to map from a person to their heart F(x)
x
person(x)  heart(F(x))  has(x,F(x))
Drop Universal Quantifiers
Distribute  over 
(A  B)  C becomes (A  C)  (A  B)
Just like distribution in arithmetic
(5 + 4) * 6
becomes (5 * 6 ) + (4 * 6 )
Flatten nested conjunctions and disjunctions.
(A  B)  C
becomes
(A  B  C)
(A  B)  C
becomes
(A  B  C)
Done!!
• Eliminate Implications
• Move  inwards
• Standardize Variables
• Move Quantifiers left
• Skolemize {Eliminate Existential Quantifiers, Drop Universal Quantifiers }
• Distribute  over 
• Flatten nested conjunctions and disjunctions.
Once we have done all the above steps, our KB is in CNF. We can now do
resolution refutation.
There is still an element of search, we have to decide which pairs of
sentences to resolve, and which substitutions we should use. The goal is
simply to find a contradiction.
There are many heuristics for the search (Our textbook lists Unit preference,
Set of support, Input resolution )
Bad News
• Even with all the heuristics resolution is exponential in general.
• Resolution is complete, but only semidecidable.
If our KB implies A (or it implies A), resolution will find the
proof in finite time. But if the KB does not implies A (or A),
resolution will simply run forever.