Inference methods in
FOL
Chapter description
• In this chapter, we describe algorithms that can answer any answerable
first-order logic
• Introduce inference rules for quantifiers and shows how to reduce
first-order inference to propositional inference, albeit at potentially great
expense.
• We describe how unification can be used to construct inference rules that
work directly with first-order sentences.
Then , we discuss three major approaches of first-order inference
algorithms:
Forward chaining ,Backward chaining and Resolution-based theorem
proving
FOL Inference
outline
• Recap
• Inference in FOL
1. Reducing first-order inference to propositional inference
Unification
Generalized Modus Ponens
2. Forward chaining
3. Backward chaining
4. Resolution (Proof by refutation )CHAP 3
FOL Inference
• Inference ?
In which we define effective procedures for
answering questions posed in first-order logic.
[Link] dogs are mammals: ∀x (Dog(x) → Mammal(x))
[Link] cats are mammals: ∀x (Cat(x) → Mammal(x))
[Link] is a dog: Dog(Fluffy)
[Link] is a cat: Cat(Whiskers)
We can use inference to answer the question:
"Is Fluffy a mammal?"
Wampus World
• the objects(constatnts) are cells in the
grid :the agent, the wumpus, and pits.
• Predicates help us express relationships
such as the agent's location, the presence
of a wumpus or pit, and adjacency
between cells.
• (Perception , action , inference )
FOL Inference
• Inference ?
[Link] dogs are mammals: ∀x (Dog(x) → Mammal(x))
[Link] cats are mammals: ∀x (Cat(x) → Mammal(x))
[Link] is a dog: Dog(Fluffy)
[Link] is a cat: Cat(Lola)
We can use inference to answer the question:
"Is Fluffy a mammal?"
FOL Inference
• Inference ?
Does
KB ⊨ α
?
a sentence follows logically from another sentence
FOL Inference
FOL recap
Reducing first-order inference to propositional inference
FOL Universal instantiation (UI)
• Notation: Subst({v/g}, α) means the result of substituting g for v in sentence α
• Every instantiation of a universally quantified sentence is entailed by it:
v α
Subst({v/g}, α)
for any variable v and ground term g
• E.g., x King(x) Greedy(x) Evil(x) yields
King(John) Greedy(John) Evil(John), {x/John}
King(Richard) Greedy(Richard) Evil(Richard), {x/Richard}
King(Father(John)) Greedy(Father(John)) Evil(Father(John)), {x/Father(John)}
FOL Existential instantiation (EI)
• For any sentence α, variable v, and constant symbol k (that does not appear elsewhere in the
knowledge base):
v α
Subst({v/k}, α)
• E.g., x Crown(x) OnHead(x,John) yields: Crown(C1) OnHead(C1,John)
•
where C1 is a new constant symbol, called a Skolem constant
• Existential and universal instantiation allows to “propositionalize” any FOL sentence or KB
• EI produces one instantiation per EQ sentence
• UI produces a whole set of instantiated sentences per UQ sentence
FOL Reduction to propositional form
Suppose the KB contains the following:
x King(x) Greedy(x) Evil(x)
Father(x)
King(John)
Greedy(John)
Brother(Richard,John)
• Instantiating the universal sentence in all possible ways, we have:
King(John) Greedy(John) Evil(John)
King(Richard) Greedy(Richard) Evil(Richard)
King(John)
Greedy(John)
Brother(Richard,John)
• The new KB is propositionalized: propositional symbols are
• King(John), Greedy(John), Evil(John), King(Richard), etc
FOL Issues with Propositionalization
1. Problem: works if α is entailed, loops if α is not entailed
2. Propositionalization generates lots of irrelevant sentences
• So inference may be very inefficient.
• E.g., consider KB
• x King(x) Greedy(x) Evil(x)
• King(John)
• y Greedy(y)
• Brother(Richard,John)
•
• It seems obvious that Evil(John) is entailed, but propositionalization produces lots of facts such as
Greedy(Richard) that are irrelevant.
3. With p k-ary predicates and n constants, there are p·nk instantiations.
4. Alternative: do inference directly with FOL sentences
FOL Unification
• Recall: Subst(θ, p) = result of substituting θ into sentence p
• Unify algorithm: takes 2 sentences p and q and returns a unifier if one exists
Unify(p, q) = θ where Subst(θ, p) = Subst(θ, q)
• Example:
p = Knows(John, x)
q = Knows(John, Jane)
Unify(p,q) = {x/Jane}
FOL Unification Examples
P=Knows(John,x) q=Knows(x,OJ)
}x/john ,x/OJ{Overloped
Unify(p,q) = {fail}
Solution
MGU = { y/John, x/z }
FOL Unfication
x King(x) Greedy(x) Evil(x)
King(John)
y Greedy(y)
Brother(Richard,John)
• We would like to infer Evil(John) without
propositionalization.
• Basic Idea: Use Modus Ponens, Resolution
when literals unify.
FOL Unification Examples
• simple example: query = Knows(John,x), i.e., who does John know?
p q θ
Knows(John,x) Knows(John,Jane) {x/Jane}
Knows(John,x) Knows(y,OJ) {x/OJ,y/John}
Knows(John,x) Knows(y,Mother(y)) {y/John,x/Mother(John)}
Knows(John,x) Knows(x,OJ) {fail}
• Last unification fails: only because x can’t take values John and OJ at the same time
• Problem is due to use of same variable x in both sentences
• Simple solution: Standardizing apart eliminates overlap of variables, e.g.,
Knows(z,OJ)
FOL Unification
• To unify Knows(John,x) and Knows(y,z),
•
θ = {y/John, x/z } or θ = {y/John, x/John, z/John}
• The first unifier is more general than the second.
• Theorem: There is a single most general unifier (MGU) that is
unique up to renaming of variables.
•
MGU = { y/John, x/z }
Unification (MGU)
• Unification algorithm
• Procedure Unify (a,b):
• – mgu := {a=b}; stop := false;
• – WHILE (not (stop) AND mgu contains s=t)
• • Case1: t is a variable, s is not a variable:
• – Replace s = t by t = s in mgu
• • Case2: s is a variable, t is the SAME variable:
• – Delete s=t from mgu
• • Case3: s is a variable, t is not a variable and contains s:
• – stop := true
• • Case4: s is a variable, t is not identical to nor contains s:
• – Replace all occurrences of s in mgu by t
• • Case5: s is of the form f(s1,…,sn), t of g(t1,…,tm):
• – If f not equal to g or m not equal to n then stop: = true
• – Else replace s=t in mgu by s1 = t1,…,sn=tn
p(f(y),w,g(z,y)) = p(x,x,g(z,A))
• MGU?
Inference Generalized Modus Ponens (GMP)
p1', p2', … , pn', ( p1 p2 … pn q)
Subst(θ,q)
Example:
King(John), Greedy(John) ,x King(x) Greedy(x) Evil(x)
Evil(John)
p1' is King(John) p1 is King(x)
p2' is Greedy(John) p2 is Greedy(x)
θ is {x/John} q is Evil(x)
Subst(θ,q) is Evil(John)
Completeness and Soundness of GMP
• GMP is sound
• Only derives sentences that are logically entailed
• GMP is complete for a 1st-order KB in Horn Clause format.
• Complete: derives all sentences that entailed.
Three main inference approaches
• Forward Chaining
• Backward Chaining
• Resolution
Three main inference approaches
• Forward Chaining =forward deduction or forward reasoning method
• Forward chaining is a form of reasoning which start with atomic
sentences in the knowledge base and applies inference rules (Modus
Ponens) in the forward direction to extract more data until a goal is
reached.
• The Forward-chaining algorithm starts from known facts =Data
Driven inference
• triggers all rules whose premises are satisfied, and add their
conclusion to the known facts (Repeatedly until goal reached )
Forward chaining algorithm
• Definite clauses disjunctions of literals of which exactly one is positive.
• P1 , p2, p3 q
Is suitable for using GMP
KB in FOL
• 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.
• Exercise: Formulate this knowledge in FOL.
KB in FOL
• ……………………………………………