Transcript Inference - Arizona State University

Inference in FOL
Chapter 9
Fall 2004
Copyright, 1996 © Dale Carnegie & Associates, Inc.
Inference with quantifiers
Previous Rules for propositional logic



Modus Ponens (p 211)
And-Elimination, plus Fig 7.11
Resolution (p 213)
(p 210)
What’s new now are variables and quantifiers

How can we reuse the above rules?
 By introducing more rules to remove V’s and Q’s
More rules with SUBST(,)


 - binding list,  - sentence
SUBST({x/Sam}, …)
 Sibling(x,John)) = Sibling(Sam,John)
CSE 471/598, CBS 598 by H. Liu
2
Inference rules for quantifiers
Universal Instantiation (UI)
For any sentence , variable v, and ground
term g,
v

SUBST ({v / g}, )
 E.g., for all greedy kings are evil
Existential Instantiation (EI)
For any , v, and constant k new to KB,
v

SUBST ({v / k}, )
 E.g., John has a crown on his head
CSE 471/598, CBS 598 by H. Liu
3
UI and EI
The new k in EI is used to name a
specific object and called a Skolem
constant in logic

If it’s not new, what would happen?
UI and EI are different in inference


UI can be applied many times
EI can be applied once, then the sentence
with EQ can be removed
 Is the new KB logically equivalent to the old KB?
 They are only inferentially equivalent
CSE 471/598, CBS 598 by H. Liu
4
Generalized Modus Ponens
p1' , p 2' ,, pn' , ( p1  p 2    pn  q)
SUBST ( , q)
It raises Modus Ponens from Prop Logic to
FOL – lifting
It takes bigger steps in inference
It’s focused - not randomly trying UIs

If we know King(John), y Greedy(y), and x
King(x) ^ Greddy(x) => Evil(x), we can apply
GMP with Θ is {x/John, y/John}, q is Evil(x), and
SUBST(Θ, q) = Evil(John)
CSE 471/598, CBS 598 by H. Liu
5
Unification
UNIFY (p,q)= (unifier - the binding list)
where SUBST(,p) = SUBST(,q)
Some examples: Unifying Knows(Jo,x) with


Knows(Jo,Ja) Knows(y,Bi) Knows(y,Mother(y))
Knows(x,Elizabeth)
Standardizing apart: Rename one sentence to
avoid name clashes
Most general unifier

Finding MGU algorithm in Fig 9.1
 Occur-Check if the variable itself occurs inside the complex
term; omitting it can result in unsound inferences
CSE 471/598, CBS 598 by H. Liu
6
An example proof
The law says that it is a crime for an American to
sell weapons to hostile nations. The country
Nono, an enemy of America, has some missiles,
and all of its missiles were sold to it by Colonel
West, who is American. (p 280)
To prove (infer) that West is a criminal.

FOL, using these predicates American, Weapon,
Sells(x,y,z), Hostile, Criminal, Owns(x,y), Missile,
Enemy(x,America)
 Datalog knowledge bases – FO definite clauses with no
function symbols

How do you prove it?
CSE 471/598, CBS 598 by H. Liu
7
Example (continued)
The proof can be very LONG for such a
simple problem if using UI (substituting with
a ground term).
The branching factor increases as KB grows.
Universal Instantiation has an enormous
branching factor.
We need more principled ways for proofs
Combining atomic sentences to conjunctions,
instantiating universal rules to match, then
applying Generalized Modus Ponens

Two ways to proceed
CSE 471/598, CBS 598 by H. Liu
8
Forward chaining
A first-order definite clause either is atomic or is
an implication p1^p2^…^p3  p

p’s are positive literals
Start with the KB and generate new conclusions
using Modes Ponens
FC is usually used when a new fact is added into
the KB, check if there are any new consequences
Algorithm FOL-FC-ASK (Fig 9.3)
An example of answering who is criminal Criminal(x) (Fig 9.4)
CSE 471/598, CBS 598 by H. Liu
9
Backward chaining
Start with something to be proved and find
implication sentences to conclude it

The list of goals is a stack waiting to be worked on
When all goals are satisfied, the proof succeeds

BC is used when there is a goal to be proved

Algorithm FOL-BC-ASK (Fig 9.6)


An example of answering who is criminal -Criminal(x)
(Fig 9.7)
BC is a depth-first search algorithm that suffers from
problems with repeated states and incompleteness
Which chaining method to use?

Any suggestion?
CSE 471/598, CBS 598 by H. Liu
10
Completeness
An incomplete proof procedure - there are
sentences entailed by the KB, the procedure cannot find
them (Fig 9.10).
Significance of completeness (Math)


All conjectures can be established mechanically
We only need a set of fundamental axioms
Significance to AI - a machine can solve any problem
that can be stated in FOL
Looking for a complete proof procedure
CSE 471/598, CBS 598 by H. Liu
11
Completeness theorem
If KB  , then KB R  - Godel’s
completeness theorem
What’s the procedure R?
“There exists one” does tell us which one
Resolution algorithm is one such procedure
Entailment in FOL is semidecidable:
We can show sentences follow, if they do;
but we can’t always show if they don’t.
CSE 471/598, CBS 598 by H. Liu
12
Resolution
A refutation complete inference procedure


Algorithm (Fig. 7.12): the same for both logics
Resolution proves KB   by proving KB^! unsatisfiable, or
by deriving the empty clause
Conjunctive normal form for FOL
Resolution inference rule
l1  l 2    lk ,
m1  m2    mn
SUBST ( , l1  ...li  1  li  1  lk  m1  ...mj  1  mj  1  mn)
where UNIFY(li, ¬mj) = 
First-order literals are complementary if one unifies with
the negation of the other
CSE 471/598, CBS 598 by H. Liu
13
Canonical forms for resolution
Conjunctive normal form (CNF)




CNF: Conjunction of disjunctions of literals
The KB is one big, implicit conjunctions
Implicative normal form (INF)
CNF and INF are notational variants
Skolemization

Eliminate existential quantifiers
 It is not as straightforward to replace with a new constant

Skolem functions
 The arguments of the Skolem function are all universally
quantified variables
CSE 471/598, CBS 598 by H. Liu
14
Conversion to normal form
1. Eliminate implications
2. Move NOT inwards
3. Standardize variables
4. Skolemize - removing E-Quantifier
introducing a function associated with the variable
5. Drop universal quantifiers
6. Distribute ^ over v
An example
 Everyone is loved by someone
 Everyone loves all animals
 Everyone who loves all animals is loved by someone
CSE 471/598, CBS 598 by H. Liu
15
Proof revisit
Criminal(West)
CSE 471/598, CBS 598 by H. Liu
16
Another example proof
Everyone who loves all animals is loved
by someone. Anyone who kills an
animal is loved by no one. Jack loves all
animals. Either Jack or Curiosity killed
the cat, who is named Tuna. Did
Curiosity kill the cat?
CSE 471/598, CBS 598 by H. Liu
17
Resolution strategies
To guide the fast proof using refutation

Unit preference
 Prefer inferences that produce shorter sentences

Set of support
 Use the negated query as the set of support

Input resolution
 Combines one of the input sentences (KB or Q)

Subsumption
 Keeps KB small by eliminating all sentences that are
subsumed by an existing sentence
CSE 471/598, CBS 598 by H. Liu
18
Summary
Simple FOL proofs are complex and
long
Generalized MP is natural and powerful,
used in forward or backward chaining
Resolution with refutation using
resolution is complete
There are strategies to guide search
CSE 471/598, CBS 598 by H. Liu
20