Inference in FOL - Arizona State University
Download
Report
Transcript Inference in FOL - Arizona State University
Inference in FOL
Chapter 9
Fall 2005
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
{x/John}, {x/Father(Richard)}
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
{x/C1}
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
Propositionalization – reducing to propositions
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 with n atomic sentences pi’
It takes bigger steps in inference
It’s focused - not randomly trying UIs
If we know King(John) – p1’, Greedy(y) – p2’, and
King(x) ^ Greddy(x) => Evil(x), we can apply
GMP with Θ is {y/John, x/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)
p, q are two sentences
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 when more than one sentence can
be unified (e.g., Knows(Jo,x), Knows(y,z))
Finding MGU algorithm in Fig 9.1
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(x),
Weapon(y), Sells(x,y,z), Hostile(z), Criminal(x),
Owns(x,y), Missile(y), 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: forward and backward
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
An example of answering who is criminal Criminal(x) (Fig 9.4)
Algorithm FOL-FC-ASK (Fig 9.3)
How fast is it?
What are side effects?
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 (the path examples 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
Or any entailed sentence has a finite proof
What’s the procedure R?
“There exists one” does NOT tell us which one
Resolution algorithm is one such procedure
Refutation-complete: if a sentence is unsatisfiable,
resolution will derive a contradiction
Entailment in FOL is semidecidable:
We can show that 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)
Negate it first …
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
A subset of sentences identified first
Work on this set
Use the negated query as the set of support
Input resolution
Combines one of the input sentences (from KB or Q) with
some other sentence (forming a single spine)
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 using UI and EI are
complex and long
Generalized Modus Ponens is natural and
powerful, used in forward or backward
chaining
Forward chaining is complete but slow
Backward chaining is focused but incomplete
Resolution with refutation is complete
There are strategies to guide search
CSE 471/598, CBS 598 by H. Liu
19