Transcript Knowledge3

1
Apatira
Uthman
2
Atphasouk
Jason
3
Chau
Minh
4
Cohen
David
5
Cook
Nathan
6
de Guzman
Armand
7
Edgcomb
Alex
8
Garcia
Steven
9
Hichborn
Geoffrey
10
Hui
Charles
11
Kazemi
Azadeh
12
Mai
Thanh
13
Millare
Brent
14
Pascua
Mark
15
Riley
Christine
16
Tasinga
Penn
17
Vu
Alexander
18
Wilhelm
Joseph
19
Ziranhua
Omar
20
Wong
Alexander
21
Phillips
Chad
22
Perkins
Dorian
23
Patthanakuha
Suphasit
2.0000000e+000 -7.3463939e+001 2.5268665e+001 4.09347
2.0000000e+000 -8.8651687e+001 4.4491863e+001 4.97600
2.0000000e+000 -3.9172705e+001 2.1531471e+001 4.37930
1.0000000e+000 -3.2314020e+001 1.8654169e+001 4.89725
2.0000000e+000 -8.3787313e+001 6.4485894e+000 2.73080
1.0000000e+000 -1.2767662e+000 -4.2687684e+001 5.1733
1.0000000e+000 -8.4865261e+001 -8.4634233e+001 5.8897
2.0000000e+000 -8.3955864e+001 4.7926503e+001 5.18295
2.0000000e+000 -6.5347533e+001 -2.3277298e+001 4.7896
Horn Form
A sentence is in Horn form if and only if ….
It is a conjunction of atomic sentences on the left side, and
a single atom on the right side
i.e.
PQRX
ABPQRX
Overview
We plan to represent the world (or some subset thereof, ie
our domain) in FOL, and to TELL this information into our
Knowledge Base KB.
We will represent our problem (ie the statement we want to
prove) in FOL. We will sometimes call the statement to be
proved a goal.
So proving a statement is equivalent to seeing if the goal is
in the KB, or if not in it, can be deduced (entailed) from it.
The simplest example
Suppose our KB consists of
P
Q
R
A simple goal is … Q. Literally we are asking is it the
case that Q is true. In this case, the answer is yes!
Another simple example
Suppose our KB consists of
P
Q
R
Now suppose the goal is … P  Q.
We are literally asking is it the case that P is true and Q
is true. In this case, the fact P  Q is not in our KB. But
we can infer it by using the And-Introduction rule.
A more interesting example
Suppose our KB consists of facts about containment
General facts about containment
•x,y,z
in(x,y)  in(y,z)  enclosedby(x,z)
•x,y
in(x,y)  enclosedby(x,y)
Specific facts for our particular problem
• in(A,B) in(B,C)
in(F,C)
Note, “in” means
directly inside with
nothing in between,
“encloses” means
inside, possibly with
other items in
between.
A
F
B
A goal might be
x enclosedby(B,x)
(ie, is there any thing inside B?)
or
x,y,z enclosedby(x,y)  enclosedby(y,z)
C
Models I
A model is simply a “world” in which a sentence is true.
Consider the sentence P  Q , given that
P
Means “is tall”.
Q
Means “is rich”.
We can now ask if the following interpretations of P  Q are
models…
“Bill Gates” is not a model of P  Q
“Eamonn Keogh” is not a model of P  Q
“Michael Jordan” is a model of P  Q
Models II
If we have the sentence P  Q, and
P
Q
Means “is astronaut”.
Means “is female”.
Which of the following interpretations of P  Q are models?
“Neil Armstrong”, “Eamonn Keogh”, “Sally Ride”, “Dolly
Parton”, “Bill Clinton”, “Valentina Tereshkova”,
Models III
Models are important because they allow a simple
definition of entailment.
A Knowledge Base KB entails a sentence  if and only if,
all models of KB are also models of .
For example the KB
PQ
…can be said to entail the sentence P  Q, since all models
of P  Q are also models of P  Q.
In propositional logic, proof is easy I
Suppose we had P and P  Q in
our KB, and we have a goal of Q
PQ
P
We can always build a truth table
with an entry for each symbol and
each item from our KB
Goal:
P
Q
PQ
FALSE
FALSE
TRUE
FALSE
TRUE
TRUE
TRUE
FALSE
FALSE
TRUE
TRUE
TRUE
We need to look at all rows where the statements in our
KB are true…
Q?
In propositional logic, proof is easy I
Suppose we had P and P  Q in our KB,
and we have a goal of Q
PQ
P
We can always build a truth table with an
entry for each symbol and each item from
our KB
P
Q
PQ
FALSE
FALSE
TRUE
FALSE
TRUE
TRUE
TRUE
FALSE
FALSE
TRUE
TRUE
TRUE
Q?
We need to look at all rows where the statements in our KB are true.
Since in every case where our KB statements are true, Q is also true, thus
we have proved Q! (I.e our KB entails Q)
All models of {P  Q , P} are also models of Q.
In FOL, proof is harder
Suppose we had P(A) and x P(x)  Q(x)
in our KB, and we have a goal of Q(A)
We can build a truth table but we cannot
fill it in.
x P(x)  Q(x)
P(A)
Q(A)?
x P(x)  Q(x)
P(A)
Q(A)
FALSE
FALSE
?
FALSE
TRUE
?
TRUE
FALSE
?
TRUE
TRUE
?
I.e. the general sentence never follows from any of these instances.
How are we to know if the KB entails the sentence Q(A)?
In the next few slides we will look at some tools that
will allow us to prove facts in First Order Logic
This tools are:
• Substitution
• Universal Elimination
• Existential Elimination
• Existential Introduction
Substitution (Binding, Instantiation)
Substitution is a variable (or set of variables) paired with a term.
Example: SUBST{x/Harpo}is a substitution indicating that Harpo
should be substituted for x.
Brother(x,Groucho)
becomes
Brother(Harpo,Groucho)
Example: SUBST{x/YoungestSonOF(Minnie)}is a substitution
indicating that YoungestSonOF(Minnie)} should be substituted for x.
Brother(x,Groucho)
becomes
Brother(YoungestSonOF(Minnie),Groucho)
Universal Elimination
(Universal Instantiation)
x 
SUBST({x/g, })
For any sentence , variable
x, and term g.
For example, from
x
loves(x, Beatles)
We can use the substitution {x/Nick} to
infer
Terms
loves(Nick, Beatles)
Or can use the substitution
{x/MotherOf(Joe) } to infer
(A term is an expression that refers to an object).
Either
• A symbol
• A function application
Symbols can be constants: John, Mary, 17, 56
or variables: F_name, L_name, X, Y
Function applications are usually written as SomethingOf
loves(MotherOf(Joe) , Beatles)
MotherOf(John)
AgeOf(Mary)
EyeColorOf(MotherOf(John))
Existential Elimination
(Existential Instantiation)
x 
SUBST({x/k, })
For any sentence , variable
x, and constant term k. Where
k does not already exist in our KB
For example from
x
President(x, USA)
We can use substitution
SUBST{x/someoldwhiteguy} to infer
Terms
(A term is an expression that refers to an object).
Either
• A symbol
• A function application
President(someoldwhiteguy, USA)
Symbols can be constants: John, Mary, 17, 56
or variables: F_name, L_name, X, Y
Later on, if we happen to learn the president is
Bush we can assign
someoldwhiteguy = Bush
Function applications are usually written as SomethingOf
MotherOf(John)
AgeOf(Mary)
EyeColorOf(MotherOf(John))
Existential Introduction

x SUBST({g/x, })
For example from
President(Bush, USA)
We can infer
x President(x, USA)
For any sentence , term g
that occurs in  and x that
does not occur in .
We can now take these new tools
• Universal Elimination
• Existential Elimination
• Existential Introduction
Combined with some tools we have already defined
To prove facts in First Order Logic
A sample proof in FOL
Bob is a buffalo
Pat is a pig
Buffaloes outrun pigs
Can Bob outrun Pat?
Buffalo(Bob)
Pig(Pat)
x,y Buffalo(x)  Pig(y)  Faster(x,y)
Faster(Bob,Pat)?
A sample proof in FOL
Can Bob outrun Pat?
Faster(Bob,Pat)?
Buffalo(Bob)
Pig(Pat)
x,y Buffalo(x)  Pig(y)  Faster(x,y)
Buffalo(Bob)  Pig(Pat)
1. We can use And Introduction to add the following to our database…
Buffalo(Bob)  Pig(Pat)
A sample proof in FOL
Can Bob outrun Pat?
Faster(Bob,Pat)?
Buffalo(Bob)
Pig(Pat)
x,y Buffalo(x)  Pig(y)  Faster(x,y)
Buffalo(Bob)  Pig(Pat)
Buffalo(Bob)  Pig(Pat)  Faster(Bob, Pat)
1. We can use And Introduction to add the following to our database…
Buffalo(Bob)  Pig(Pat)
2. We can do Universal Elimination to get…
{x/Bob, y/Pat} Buffalo(Bob)  Pig(Pat)  Faster(Bob, Pat)
A sample proof in FOL
Can Bob outrun Pat?
Faster(Bob,Pat)?
Buffalo(Bob)
Pig(Pat)
x,y Buffalo(x)  Pig(y)  Faster(x,y)
Buffalo(Bob)  Pig(Pat)
Buffalo(Bob)  Pig(Pat)  Faster(Bob, Pat)
Faster(Bob, Pat)
1. We can use And Introduction to add the following to our database…
Buffalo(Bob)  Pig(Pat)
2. We can do Universal Elimination to get…
{x/Bob, y/Pat} Buffalo(Bob)  Pig(Pat)  Faster(Bob, Pat)
3. We then use Modus Ponens to derive
Faster(Bob, Pat)
The need for a better proof mechanism
The proof mechanism we have just seen can be imagined as search.
The operators are inference rules (Existential Introduction, Universal Elimination, etc)
The states are set of sentences (The KB itself)
The goal test is to see if a state contains the query sentence.
This idea works, but…
It seriously slows down when the KB gets larger, because the
number of possible substitutions grows exponentially.
One possible solution is to reduce the number of operators…
This leads us to Generalized Modus Ponens (GMP).
Generalized Modus Ponens
Combines And-Introduction, Universal-Elimination, and Modus Ponens
For atomic sentences p1’, p2’, and q, where there is a
substitution  such that SUBST({/ pi’ }) = SUBST({/ pi})
p1’, p2’,…pn’ (p1  p2… pn  q )
SUBST({/q})
Example:
p1’ = Faster(Bob,Pat)
p2’ = Faster(Pat,Steve)
p1  p2  q = Faster(x,y)  Faster(y,z)  Faster(x,z)
SUBST({/q}) = SUBST({x/Bob, y/Pat, z/Steve })
Then using GMP we can conclude Faster(Bob,Steve)
Note that GMP only works for a KB of definite clauses (Exactly one positive literal): either
a single atom or (conjunction of atomic sentences)  atomic sentence
Sentences in this form are known as horn clauses.
Note also that all sentences are assumed to be universally qualified
Generalized Modus Ponens
Combines And-Introduction, Universal-Elimination, and Modus Ponens
For atomic sentences p1’, p2’, and q, where there is a
substitution  such that SUBST({/ pi’ }) = SUBST({/ pi})
p1’, p2’ (p1  p2  q )
SUBST({/q})
Example:
p1’ = Faster(Bob,Pat)
p2’ = Faster(Pat,Steve)
p1  p2  q = Faster(x,y)  Faster(y,z)  Faster(x,z)
SUBST({/q}) = SUBST({x/Bob, y/Pat, z/Steve })
Then using GMP we can conclude Faster(Bob,Steve)
Faster(Bob,Pat)  Faster(Pat,Steve)  Faster(Bob,Steve)


Forward Chaining
Proofs start with the given axioms/premises in KB, deriving new sentences using GMP until
the goal/query sentence is derived. This defines a forward chaining inference procedure
because it moves "forward" from the KB to the goal.
Example: KB = All cats like fish, cats eat everything they like, and
Ziggy is a cat. In FOL, KB =
1. x cat(x)  likes(x, Fish)
2. x y (cat(x)  likes(x,y))  eats(x,y)
3. cat(Ziggy)
Goal query: Does Ziggy eat fish?
Proof:
4. Use GMP with (1) and (3) to derive: 4. likes(Ziggy, Fish)
5. Use GMP with (3), (4) and (2) to derive eats(Ziggy, Fish)
6. So, Yes, Ziggy eats fish.
Backward Chaining
Backward-chaining deduction using GMP is complete for KBs containing only Horn clauses. Proofs start
with the goal query, find implications that would allow you to prove it, and then prove each of the
antecedents in the implication, continuing to work "backwards" until we get to the axioms, which we know
are true.
Example: Does Ziggy eat fish?
To prove eats(Ziggy, Fish), first see if this is known from one of the axioms directly. Here it is
not known, so see if there is a Horn clause that has the consequent (i.e., right-hand side) of the
implication matching the goal. Here,
1. x cat(x)  likes(x, Fish)
2. x y (cat(x)  likes(x,y))  eats(x,y)
3. cat(Ziggy)
Proof:
1.Goal matches RHS of Horn clause (2), so try and prove new sub-goals
cat(Ziggy) and likes(Ziggy, Fish) that correspond to the LHS of (2)
2.cat(Ziggy) matches axiom (3), so we've "solved" that sub-goal
3.likes(Ziggy, Fish) matches the RHS of (1), so try and prove cat(Ziggy)
4.cat(Ziggy) matches (as it did earlier) axiom (3), so we've solved this sub-goal
5.There are no unsolved sub-goals, so we're done. Yes, Ziggy eats fish.
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).
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.
Gloss over!
Note that we must do the steps in order!
Eliminate Implications
Change all implication sentences to disjunctions
So
AB
Gloss
A  Bover!
becomes
C  D becomes
etc
C  D
Move  inwards
Negation is only allow on atom, not whole sentences.
So
Gloss
A over!
B
(A  B) becomes
(A  B)
becomes
A  B
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).
Gloss over!
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)
Gloss over!
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
SUBST{x/A}
P(A)  Q(A)
Gloss over!
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)
Gloss over!
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
Gloss
over!
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.