FOL Inference
AIMA 9
CMPSC 442
Week 6, Meeting 18, Four Segments
Outline
● Propositional and First-Order Inference
● Unification and First-Order Inference
● Forward Chaining vs. Backward Chaining
● Resolution in FOL
2Outline, Wk 6, Mtg 18
FOL Inference
AIMA 9
CMPSC 442
Week 6, Meeting 17, Segment 1 of 4: Propositional and
First-Order Inference
Convert FOL to PL Then do Inference
● Propositionalize the FOL
○ Eliminate quantifiers
○ Skolemize
● Semidecidability
○ Theorem: any sentence entailed by FOL KB is entailed by a finite subset of
the propositionalized KB
○ Problem: a sentence not entailed by FOL cannot be recognized as
unprovable in the propositionalized KB
4PL and FOL Inference
Universal and Existential Instantiation
● Replace quantified sentences with instantiated sentences
○ Variables are replaced with constants
○ Not with the “objects” of a model
● Inferentially equivalent to the original quantified sentences
● New KB’ is satisfiable whenever KB is satisfiable
● Can use propositional inference on KB’
5PL and FOL Inference
Universal Instantiation (UI)
● Every instantiation of a universally quantified sentence is entailed by it
● For any variable v and ground term g (or constant; not domain object):
● The constant is the “name” of the domain object
● Apply UI to: ∀x King(x) ∧ Greedy(x) ⇒ Evil(x)
○ King(John) ∧ Greedy(John) ⇒ Evil(John)
. . .
6PL and FOL Inference
Existential Instantiation (EI)
● For any sentence σ, variable v, and constant symbol k that does not
appear elsewhere in the knowledge base:
● Apply EI to: ∃x Crown(x) ∧ OnHead(x,John)
○ Crown(C
1
) ∧ OnHead(C
1
,John)
○ Provided C
1
is a new constant symbol (a new name, not already used)
○ C
1
is called a Skolem constant (skolemization)
7PL and FOL Inference
Reduction to Propositional Inference
● Every FOL KB can be propositionalized so as to preserve entailment
○ A ground sentence α is entailed by new KB’ iff entailed by original KB
● Idea: propositionalize KB and query, apply resolution, return result
● Problem: with function symbols, an infinite number of ground terms can
be generated
○ Father(Father(Father(John)))
8PL and FOL Inference
Semi-decidability of Propositionalized KB
● Theorem (Herbrand, 1930): If a sentence α is entailed by an FOL KB, it
is entailed by a finite subset of the propositionalized KB
● For n = 0 to ∞ do
○ create a propositional KB by instantiating with depth-n terms
○ see if α is entailed by this KB
● Problem: works if α is entailed, loops if α is not entailed at a finite n
● Theorem (Turing, 1936; Church, 1936) Entailment for FOL is
semi-decidable
○ Algorithms exist that prove every entailed sentence
○ No algorithm exists that also disproves every non-entailed sentence
9PL and FOL Inference
Other Problems with Propositionalization
● Will lead to generation of (numerous!) irrelevant sentences
● With p k-ary predicates and n constants, there are pnk instantiations
● Very inefficient!
10PL and FOL Inference
FOL Inference
AIMA 9
CMPSC 442
Week 6, Meeting 17, Segment 2 of 4: Unification
Unification Increases Efficiency
● Instead of instantiation, find a substitution for variables in the KB
○ Make the conjuncts in an implication match atomic statements in the KB
○ Find substitutions for quantified statements
● {x/John, y/John} will satisfy the premises, leading to the conclusion that
John is evil
12
Generalized Modus Ponens (GMP)
● Efficient inference of Evil(John) from
○ ∀x King(x) ∧ Greedy(x) ⇒ Evil(x)
○ King(John)
○ ∀y Greedy(y)
● GMP: Find a substitution Subst({x/John, y/John})
○ Where the KB facts match the premises of the implication
■ King(John)
■ Greedy(John)
○ Derive the consequent with the substitution, Evil(John)
13Unification
GMP More Formally
● Given:
○ An implication (p1 ∧ p2 ∧… ∧ pn ) ⇒ q
○ Each of its premises p1’, p2’, . . . , pn ’
○ A substitution θ such that Subst(θ, pi) = Subst(θ, pi’) for all i
14Unification
Soundness of GMP
● Provided that
● Need to show:
● Lemma: for any sentence p, we have p ⊨ pθ by UI
○ E
○ Ef
○ From the above, qθ follows by ordinary Modus Ponens
F
15Unification
GMP and FOL
● GMP is a lifted Modus Ponens
● Raises Modus Ponens from variable-free propositional logic to FOL
● Inference in FOL – Lifted versions of
○ Forward Chaining
○ Backward Chaining
○ Resolution
16Unification
Unification: Systematic Substitution
● Given two logical statements p, q
● Find a substitution θ (unifier) that make p and q look identical
Unify(p, q) = θ where Subst(θ,p) = Subst(θ,q)
● A key component of first order inference algorithms
17Unification
Unification Example
● Query: Who does John know?
AskVars(Knows(John,x))
● Find all sentences in the KB that unify with Knows(John,x)
18
p q θ
Knows(John,x) Knows(John,Jane) {x/Jane}
Knows(John,x) Knows(y,Bill) {y/Bill}
Knows(John,x) Knows(y,Mother(y)) {y/John, x/Mother(John)}
Knows(John,x) Knows(x,Elizabeth) failure
Unification
Standardizing Apart
● There is no substitution for the first row that tell us who John knows,
because x cannot be the person John knows in the first statement (p),
and John in the second statement (q)
● Standardizing apart means to use different variables in different
statements to avoid name clashes
19
p q θ
Knows(John,x) Knows(x,Elizabeth) Cannot use the same var
Knows(John,x) Knows(y,Elizabeth) {x/Elizabeth, y/John}
Unification
Most General Unifier (MGU)
● To unify Knows(John,x) and Knows(y,z):
θ1 = {y/John, x/z } or θ2 = {y/John, x/John, z/John}
● The first unifier is more general than the second (less restrictive)
● There is a single most general unifier (MGU) that is unique up to
renaming of variables
○ MGU = {y/John, x/z}
○ Knows(John,z) = Knows(John,z)
20Unification
Unification Algorithm
21Unification
Unification Algorithm: Unify-Var
22UnificationUnification
Logic Programming through Unification Algorithms
● Prolog
○ Developed in the 1970’s
■ Alain Colmeraouer, University of Aix-Marseille
■ Robert Kowalski, University of Edinburgh
○ In wide use throughout the ‘70’s through ‘90’s
■ Natural Language Processing applications
■ Knowledge Representation and Reasoning
■ Has features that are inconsistent with pure logic programming (cut())
● Datalog
● Mercury
23Unification
FOL Inference
AIMA 9
CMPSC 442
Week 6, Meeting 17, Segment 3 of 4: Forward and
Backward Chaining
FOL Example
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.
● Prove that Col. West is a criminal
● Convert text to first-order definite clauses
○ Atomic clause
○ Implication whose antecedent is a conjunction of positive literals, whose
consequent is a positive literal
○ No existential quantification
○ Statements with variables are implicitly universally quantified
25Forward & Backward Chaining
Conversion to Definite Clauses
1. The law says that it is a crime for Americans to sell weapons to hostile
nations.
2. The country Nono, an enemy of America, has some missiles, and all of
its missiles were sold to it by Colonel West, who is an American.
26Forward & Backward Chaining
More Facts for the Colonel West KB
27
And-Elimimation
Definitions
EI; Skolemization
Forward & Backward Chaining
Forward Chaining Proof: Assert the Atomic Facts
28Forward & Backward Chaining
Forward Chaining Proof: Apply Modus Ponens
29Forward & Backward Chaining
Forward Chaining Proof: Apply Modus Ponens
30Forward & Backward Chaining
Forward Chaining
● Sound and complete for Datalog
● Datalog = first-order definite clauses + no functions
● Forward chaining terminates for Datalog in finite number of iterations
● May not terminate in general if α is not entailed
○ Recall: Entailment with definite clauses is semidecidable
31Forward & Backward Chaining
Efficiency of Forward Chaining
● Incremental forward chaining: no need to match a rule on iteration k if
a premise wasn’t added on iteration k-1
○ Match each rule whose premise contains a newly added positive literal
○ Problem: matching can be expensive: polynomial
○ Solution: database indexing allows linear time retrieval of known facts
● Forward chaining is widely used in deductive databases
32Forward & Backward Chaining
Backward Chaining Proof
33Forward & Backward Chaining
Backward Chaining Proof
34Forward & Backward Chaining
Backward Chaining Proof
35Forward & Backward Chaining
Backward Chaining Proof
36Forward & Backward Chaining
Backward Chaining Proof
37Forward & Backward Chaining
Backward Chaining Proof
38Forward & Backward Chaining
Backward Chaining Proof
39Forward & Backward Chaining
Backward Chaining Proof
40Forward & Backward Chaining
Backward Chaining Proof
41Forward & Backward Chaining
Backward Chaining
● Depth-first recursive proof search: space is linear in size of proof
● Incomplete due to infinite loops
○ Fix: checking current goal against every goal on stack
● Inefficient due to repeated subgoals (both success and failure)
○ Fix: use caching of previous results (extra space)
● Widely used for logic programming
42Forward & Backward Chaining
FOL Inference
AIMA 9
CMPSC 442
Week 6, Meeting 17, Segment 4 of 4: Resolution
Using Resolution in FOL
● KB must be in CNF
● Yields a complete inference procedure
● Efficient inference strategies exist
● Similar to conversion of PL to CNF; differences due to quantifiers
○ Implication elimination
○ Move ¬ inwards
○ Standardize variables
○ Skolemize: remove existential quantification
○ Drop universal quantifiers
○ Distribute ∨ over ∧
44Resolution
Example Conversion of FOL to CNF
● FOL Sentence
● CNF Translation
45Resolution
Resolution Inference Rule: Lifted version of PL
● The two premises are standardized apart (no variables in common)
● Resolution inference as in PL: Proof by contradiction
46Resolution
Colonel West Example in CNF
47Resolution
Colonel West Example: Resolution Proof
48Resolution
Summary: Page One
● Initial type of FOL inference: use UI and EI to propositionalize the KB,
then use the same type of inference as for PL; simple but slow
● Use of unification to identify appropriate substitutions for variables
eliminates the instantiation step, making inference more efficient
● A lifted version of Modus Ponens, Generalized Modus Ponens, relies
on unification
○ Forward Chaining and Backward Chaining algorithms apply this rule to
FOL KBs in definite clause form
○ GMP is complete for definite clauses
○ Entailment is semidecidable
49Summary, Wk 6, Mtg 18
Summary: Page Two
● Forward chaining is complete for Datalog, runs in polynomial time
● Backward chaining is used in logic programming
○ Suffers from redundant inferences, infinite loops
○ Prolog: logic programming with some non-logical elements
■ Uses a closed world/unique names assumption, negation as failure
■ Cut
● Generalized resolution inference for CNF form provides a complete
proof system for FOL
50Summary, Wk 6, Mtg 18