Transcript W7 - Arizona State University

Inference in FOL
Chapter 9
Spring 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)
Variables and quantifiers
More rules with SUBST(,)


 - binding list,  - sentence
SUBST({x/Sam}, …)
 Sibling(x,John)) = Sibling(Sam,John)
CS 471/598 by H. Liu
2
Inference rules for quantifiers
Universal Instantiation (UI)
For any sentence , variable v, and ground
v

term g,
SUBST ({v / g}, )

E.g.,
Existential Instantiation (EI)
For any , v, and constant k new to KB,
v

SUBST ({v / k}, )
 E.g.,
CS 471/598 by H. Liu
3
Generalized Modus Ponens
p1' , p 2' ,, pn' , ( p1  p 2    pn  q)
SUBST ( , q)
It raises Modus Ponens from Prop Logic to
FOL – it’s called lifting
It takes bigger steps in inference
It’s focused - not randomly trying UIs
CS 471/598 by H. Liu
4
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
CS 471/598 by H. Liu
5
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, Hostile, Criminal, Owns, Missile, Enemy
 Datalog knowledge bases – FO definite clauses with no
function symbols

How do you prove it?
CS 471/598 by H. Liu
6
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
CS 471/598 by H. Liu
7
Forward chaining
A first-order definite clause either is atomic or is
an implication p1^p2^…^p3  p


p’s are positive literals
Datalog KBs – FO DC without function symbols
Start with the KB and generate new conclusions
using Modes Ponens
FC is usually used when a new fact is added into
the KB -> any new consequences
Algorithm FOL-FC-ASK (Fig 9.3)
An example of answering who is criminal Criminal(x) (Fig 9.4)
CS 471/598 by H. Liu
8
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?
CS 471/598 by H. Liu
9
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
CS 471/598 by H. Liu
10
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.
CS 471/598 by H. Liu
11
Resolution
A refutation complete inference procedure

Algorithm (Fig. 7.12): the same for both logics
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
CS 471/598 by H. Liu
12
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 existstential quantifiers
Skolem functions
 The arguments of the Skolem function are all universally
quantified variables
CS 471/598 by H. Liu
13
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 who loves all animals is loved by someone
CS 471/598 by H. Liu
14
Proof revisit
Criminal(West)
CS 471/598 by H. Liu
15
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?
CS 471/598 by H. Liu
16
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
CS 471/598 by H. Liu
17
Summary
Simple FOL proofs are complex and
long
Generalized MP is natural and powerful,
used in forward or backward chaining
Generalized resolution is more general
than generalized MP, but not complete
Refutation using resolution is complete
There are strategies to guide search
CS 471/598 by H. Liu
19