Week 11: Unification, Generalized Modus
Download
Report
Transcript Week 11: Unification, Generalized Modus
Let us think of interpretations for FOPC that are more
like interpretations for prop logic
Herbrand Interpretations
•
Herbrand Universe
– All constants
• Rao,Pat
– All “ground” functional terms
• Son-of(Rao);Son-of(Pat);
• Son-of(Son-of(…(Rao)))….
•
x, y Friend ( x, y ) Likes( x, y )
Friend ( Rao , Pat )
Friend ( Pat , son of ( Rao ))
Herbrand Base
– All ground atomic sentences made with
terms in Herbrand universe
• Friend(Rao,Pat);Friend(Pat,Rao);Friend(P
at,Pat);Friend(Rao,Rao)
• Friend(Rao,Son-of(Rao));
• Friend(son-of(son-of(Rao),son-of(sonof(son-of(Pat))
– We can think of elements of HB as
propositions; interpretations give T/F
values to these. Given the interpretation,
we can compute the value of the FOPC
database sentences
If there are n constants; and
p k-ary predicates, then
--Size of HU = n
--Size of HB = p*nk
But if there is even one function,
then |HU| is infinity and so is |HB|.
--So, when there are no function
symbols, FOPC is really just
syntactic sugaring for a (possibly
much larger) propositional database
But what about Godel?
• In First Order Logic
– We have finite set of constants
– Quantification allowed only over variables…
• Godel’s incompleteness theorem holds only in a system that includes
“mathematical induction”—which is an axiom schema that requires
infinitely many FOPC statements
– If a property P is true for 0, and whenever it is true for number n, it is also
true for number n+1, then the property P is true for all natural numbers
– You can’t write this in first order logic without writing it once for each P
(so, you will have to write infinite number of FOPC statements)
• So, a finite FOPC database is still semi-decidable in that we can prove
all provably true theorems
Proof-theoretic
Inference in first order logic
•
For “ground” sentences (i.e., sentences without any quantification), all the old
rules work directly (think of ground atomic sentences as propositions)
– P(a,b)=> Q(a); P(a,b) |= Q(a)
– ~P(a,b) V Q(a) resolved with P(a,b) gives Q(a)
•
What about quantified sentences?
– May be infer ground sentences from them….
– Universal Instantiation (a universally quantified statement entails every
instantiation of it)
xyP( x, y ) Q( x)entailsP (a, b) Q(a)
– Existential instantiation (an existentially quantified statement holds for some term
(not currently appearing in the KB).
•
xP( x) entails P( SK1) sk1 is a new const.
Can we combine these (so we can avoid unnecessary instantiations?) Yes.
Generalized modus ponens
xyP( x, y ) Q( x); P(a, b) entails q(b)
•
Needs UNIFICATION
UI can be applied several
times to add new sentences
--The resulting KB is
equivalent to the old one
EI can only applied once
--The resulting DB is
not equivalent to the
old one
BUT will be satisfiable
only when the old one is
Want mgu (maximal general unifiers)
How about knows(x,f(x)) knows(u,u)?
x/u; u/f(u)leads to infinite regress (“occurs check”)
GMP can be used in the “forward” (aka “bottom-up”) fashion
where we start from antecedents, and assert the consequent
or in the “backward” (aka “top-down”) fashion where we start
from consequent, and subgoal on proving the antecedents.
Apt-pet
• An apartment pet is a pet
that is small
• Dog is a pet
• Cat is a pet
• Elephant is a pet
• Dogs, cats and skunks are
small.
• Fido is a dog
• Louie is a skunk
• Garfield is a cat
• Clyde is an elephant
• Is there an apartment pet?
1.small ( x) pet ( x) aptPet( x)
2.dog ( x) pet ( x)
3.cat ( x) pet ( x)
4.elephant ( x) pet ( x)
5.skunk ( x) small ( x)
6.cat ( x) small ( x)
7.dog ( x) small ( x)
8.dog ( fido)
9.skunk (louie )
10.cat ( garfield )
11.elephant (clyde )
? aptPet( x)
1.small ( x) pet ( x) aptPet( x)
2.dog ( x) pet ( x)
3.cat ( x) pet ( x)
4.elephant ( x) pet ( x)
5.skunk ( x) small ( x)
6.cat ( x) small ( x)
7.dog ( x) small ( x)
8.dog ( fido)
9.skunk (louie )
10.cat ( garfield )
11.elephant (clyde )
? aptPet( x)
Efficiency can be improved by re-ordering subgoals adaptively
e.g., try to prove Pet before Small in Lilliput Island; and
Small before Pet in pet-store.
Similar to “Integer Programming” or “Constraint Programming”
Generate compilable
matchers for each
pattern, and use them
Example of FOPC Resolution..
Everyone is loved by someone
xy loves( y, x) loves( SK ( x' ), x' )
If x loves y, x will give a valentine card to y
xy loves( y, x) GV ( y, x) loves( y, x) GV ( y, x)
Will anyone give Rao a valentine card?
zGV ( z, Rao ) zGV ( z, Rao ) zGV ( z, Rao ) GV ( z, Rao )
y/z;x/Rao
~loves(z,Rao)
z/SK(rao);x’/rao
Finding where you left your key..
Atkey(Home) V Atkey(Office) 1
Where is the key?
Ex Atkey(x)
Negate
Forall x ~Atkey(x)
CNF ~Atkey(x) 2
Resolve 2 and 1 with x/home
You get Atkey(office) 3
Resolve 3 and 2 with x/office
You get empty clause
So resolution refutation “found”
that there does exist a place
where the key is…
Where is it?
what is x bound to?
x is bound to office once
and home once.
so x is either home or office
Existential proofs..
• Are there irrational numbers p and q such
that pq is rational?
2
2
2
pq 2
2
2
2
p 2 q 2
This and the previous examples
show that resolution refutation is
powerful enough to model
existential proofs.
In contrast, generalized modus
ponens is only able to model
constructive proofs..
Existential proofs..
• The previous example shows that resolution
refutation is powerful enough to model existential
proofs. In contrast, generalized modus ponens is
only able to model constructive proofs..
• (We also discussed a cute example of existential
proof—is it possible for an irrational number
power another irrational number to be a rational
number—we proved it is possible, without
actually giving an example).
GMP vs. Resolution Refutation
• While resolution refutation is a complete inference for
FOPC, it is computationally semi-decidable, which is a far
cry from polynomial property of GMP inferences.
• So, most common uses of FOPC involve doing GMP-style
reasoning rather than the full theorem-proving..
• There is a controversy in the community as to whether the
right way to handle the computational complexity is to
– a. Develop “tractable subclasses” of languages and require the
expert to write all their knowlede in the procrustean beds of those
sub-classes (so we can claim “complete and tractable inference”
for that class) OR
– Let users write their knowledge in the fully expressive FOPC, but
just do incomplete (but sound) inference.
– See Doyle & Patil’s “Two Theses of Knowledge Representation”