Ch.
9 Inference in First-Order Logic
Conversionto CNF
conjuntivenormalform
Inference in First-Order Logic
9.1. Propositional vs. First-Order Inference
9.1.1. Inference rules for quantifiers
9.1.2. Reduction to propositional inference
9.2. Unification and Lifting
9.2.1. A first-order inference rule
9.2.2. Unification
9.2.3. Storage and retrieval
9.3. Forward Chaining
9.3.1. First-order definite clauses
9.3.2. A simple forward-chaining algorithm
9.3.3. Efficient forward chaining
Matching rules against known facts
Incremental forward chaining
Irrelevant facts
Inference in First-Order Logic
9.4. Backward Chaining
9.4.1. A backward-chaining algorithm
9.4.2. Logic programming
9.4.3. Efficient implementation of logic programs
9.4.4. Redundant inference and infinite loops
9.4.5. Database semantics of Prolog
9.4.6. Constraint logic programming
9.5. Resolution
9.5.1. Conjunctive normal form for first-order logic
9.5.2. The resolution inference rule
9.5.3. Example proofs
9.5.4. Completeness of resolution
9.5.5. Equality
9.5.6. Resolution strategies
Practical uses of resolution theorem provers
A Brief History of Reasoning
Universal Instantiation (UI)
• Every instantiation of a universally quantified sentence is
entailed by it:
• For any variable v and ground trem g
• E.g. ∀x King(x) ∧ Greedy(x) ⇒ Evil(x) yields
– King(John) ∧ Greedy(John) ⇒ Evil(John)
– King(Richard) ∧ Greedy(Richard) ⇒ Evil(Richard)
– …
Existential Instantiation (EI)
• For any sentence α, variable v, and constant symbol k that does not appear
elsewhere in the knowledge base:
• ∃ x Crown(x) ∧ OnHead(x, John)
– Crown(C1) ∧ OnHead(C1, John)
Provided C1 is a new constant symbol, called a Skolem constant
• UI can be applied several times to add new sentences; the new KB is
logically equivalent to the old
• EI can be applied once to replace the existential sentence: the new KB is
not equivalent to the old, but is satisfiable iff the old KB was satisfiable
Reduction to Propositional Inference
• Suppose the KB contains just the following:
– ∀x King(x) ∧ Greedy(x) ⇒ Evil(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:
– proposition symbols are
King(John), Greedy(John), Evil(John), King(Richard), etc.
Reduction to Prop. Inference (cont.)
• Claim
– a ground sentence is entailed by new KB iff entailed by original KB
– every FOL KB can be propositionalized so as to preserve entailment
• Idea
– propositionalize KB
– query, apply resolution, return result
• Problem
– with function symbols, there are infinitely many ground terms,
– e.g., Father(Father(Father(John)))
Reduction to Prop. Inference (cont.)
• Theorem (Herbrand, 1930)
– If a sentence α is entailed by an FOL KB, it is entailed by a finite subset of
the propositional KB
• Idea
– For n = 0 to 1 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
• Theorem (Turing, 1936), (Church, 1936)
– entailment in FOL is semidecidable
Problems with Propositionalization
• Propositionalization seems to generate lots of irrelevant sentences.
• E.g., from ∀x King(x) ∧ Greedy(x) ⇒ Evil(x)
– King(John)
– ∀y Greedy(y)
– Brother(Richard, John)
• It seems obvious that Evil(John), but propositionalization produces lots of
facts such as Greedy(Richard) that are irrelevant
• With p k-ary predicates and n constants, there are p · nk instantiations
• With function symbols, it gets much worse
Unification
• We can get the inference immediately if we can find a substitution
θ such that
– King(x) and Greedy(x) match King(John) and Greedy(y)
θ = {x/John, y=John} works UNIFY(α, β) = θ if αθ = βθ
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
• Standardizing apart eliminates overlap of variables
– E.g. Knows(z17, OJ)
0 - ⽤ Fn 表⽰
Generalized Modus Ponens (GMP)
01
它 的 Substution 是 XIJ ohn
Q
glxtgihnwwnrn
它 的 Substution 是
結論
眾多 東⻄ 的 or 只有 ⼀個 為 正 GAVBUCWDJ
Example Knowledge Base
• 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. [Link] n Missiks IMD
• Prove that Col. West is a criminal.
Resolution 的 步驟
Example Knowledge Base (cont.)
• … it is a crime for an American to sell weapons to hostile nations.
– American(x) ∧ Weapon(y) ∧ Sells(x,y,z) ∧ Hostile(z) ⇒ Criminal(x)
• Nono, an enemy of America, has some missiles
– Owns(Nono, M1) ∧ Missile(M1)
• all of its missiles were sold to it by Colonel West
– ∀x Missle(x) ∧ Owns(Nono, x) ⇒ Sells(West, x, Nono)
• Missiles are weapons
– Missile(x) ⇒ Weapon(x)
• An enemy of America counts as “hostile”
– Enemy(x, America) ⇒ Hostile(x)
• West, who is American
– American(West)
• The country Nono, an enemy of America
– Enemy(Nono, America)
Figure 9.3 Forward Chaining Algorithm
(p.332)
Figure 9.4 Forward Chaining Proof
(p.332)
Implīcations
_
Facts
①
Ownsl Nono ,
MI )
① Americanlx)
Hostīlelz)
Weaponly)
>
=
Criminal 以
sellsyy Lmplications
② Missile ( M 2) 》 Missīk ⼼
Ownslnono
③
Americanlwestj Selkl West
, x
, Nono )
, xj
Missilelx)
[Link]@[Link]
④ ③
weaponl 》
ican )
Hostik ID
Facts
Efficiency of Forward Chaining
• Simple observation
– 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 literal
– Matching itself can be expensive
• Database indexing
– allows O(1) retrieval of known facts
– e.g., query Missile(x) retrieves Missile(M1)
• Matching conjunctive premises against known facts is NP-hard
• Forward chaining is widely used in deductive databases
Figure 9.5 Hard Matching Example
(p.334)
• Colorable() is inferred iff the CSP has a solution
• CSPs include 3-SAT (3-satisfiability) as a special case, hence
matching is NP-hard
Figure 9.6 Backward Chaining Algorithm
(p.338)
Figure 9.7 Backward Chaining Example
(p.338)
Crimindl
MDFS
節省 效率
o
Facts
Properties of Backward Chaining
• Depth-first recursive proof search DFS
– space is linear in size of proof
• Incomplete due to infinite loops 無 窮 迴圈
– fix by checking current goal against every goal on stack
• Inefficient due to repeated subgoals (both success and failure)
(
– fix using caching of previous results (extra space!)
• Widely used (without improvements!) for logic programming
在 不同 位置 間 相同 的 變數
Logict Control
Algorithm ⼆
Logic Programming
Computation as inference on logical KBs
• Logic programming 無須 找 solution • Ordinary programming
1. Identify problem 1. Identify problem
2. Assemble information 2. Assemble information
3. Tea break 3. Figure out solution
4. Encode information in KB 4. Program solution
5. Encode problem instance as facts 5. Encode problem instance as data
6. Ask queries 6. Apply program to data
7. Find false facts 7. Debug procedural error
Prolog
Resolution
Conversion to CNF
• Everyone who loves all animals is loved by someone
∀x [∀y Animal(y) ⇒ Loves(x,y)] ⇒ [∃y Loves(y,x)]
1. Eliminate biconditionals and implications
∀x [∀y ¬ Animal(y) ∨ Loves(x,y)] ⇒ [∃y Loves(y,x)]
∀x ¬[∀y ¬ Animal(y) ∨ Loves(x,y)] ∨ [∃y Loves(y,x)]
2. Move ¬ inwards (¬∀x p ≡ ∃x ¬p) (¬∃x p ≡ ∀x ¬p)
∀x [∃y ¬(¬ Animal(y) ∨ Loves(x,y))] ∨ [∃y Loves(y,x)]
∀x [∃y Animal(y) ∧ ¬ Loves(x,y)] ∨ [∃y Loves(y,x)]
3. Standardize variables
∀x [∃y Animal(y) ∧ ¬ Loves(x,y)] ∨ [∃z Loves(z,x)]
Conversion to CNF (cont.)
• Everyone who loves all animals is loved by someone
∀x [∀y Animal(y) ⇒ Loves(x,y)] ⇒ [∃y Loves(y,x)]
4. Skolemize (more general form of existential instantiation)
f) ∧ ¬ Loves(x,F(x))]
O ∨ [Loves(G(x),x)]
Dskolemfunction
∀x [Animal(F(x))
5. Drop universal quantifiers
∧ ¬ Loves(x,F(x))] ∨ [Loves(G(x),x)]
[Animal(F(x))0
6. Distribute ∧ over ∨
ro
[Animal(F(x)) ∨ Loves(G(x),x)] ∧ [ Loves(x,F(x)) ∨ Loves(G(x),x)]
Example on Selling Weapons
• … it is a crime for an American to sell weapons to hostile nations.
– American(x) ∧ Weapon(y) ∧ Sells(x,y,z) ∧ Hostile(z) ⇒ Criminal(x)
• Nono, an enemy of America, has some missiles
– Owns(Nono, M1) ∧ Missile(M1)
• all of its missiles were sold to it by Colonel West
– ∀x Missle(x) ∧ Owns(Nono, x) ⇒ Sells(West, x, Nono)
• Missiles are weapons
– Missile(x) ⇒ Weapon(x)
• An enemy of America counts as “hostile”
– Enemy(x, America) ⇒ Hostile(x)
• West, who is American
– American(West)
• The country Nono, an enemy of America
– Enemy(Nono, America)
Example on Selling Weapons
• American(x) ∧ Weapon(y) ∧ Sells(x,y,z) ∧ Hostile(z) ⇒
Criminal(x) x > p =
= -
xvp
• Owns(Nono, M1) ∧ Missile(M1)
• ∀x Missle(x) ∧ Owns(Nono, x) ⇒ Sells(West, x, Nono)
• Missile(x) ⇒ Weapon(x)
• Enemy(x, America) ⇒ Hostile(x)
• American(West)
• Enemy(Nono, America)
Example Proof
• Given statements
– ¬American(x) ∨ ¬Weapon(y) ∨ ¬Sells(x, y, z) ∨ ¬Hostile(z) ∨ Criminal(x)
– ¬Missile(x) ∨ ¬Owns(Nono, x) ∨ Sells(West, x, Nono)
– ¬Enemy(x, America) ∨ Hostile(x)
– ¬Missile(x) ∨ Weapon(x)
– Owns(Nono, M1)
– Missile(M1)
– American(West)
– Enemy(Nono, America)
• General goal
– ¬Criminal(West)
Figure 9.11 Example Proof
(p.348)
ˊ ˊ
⼆ ⼆
⼆ ⼆
⼆ ⼆
ˊ ˊ
ˊ
á
Example 2
{
• 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? [Link] _ ⺣ → p…
gǎnnng …
吼
Sis P ltx 11
[Link]
No
Sisnot P (⼆ [Link] DJ
Conversatīonto CNF
Example 2
• Everyone who loves all animals is loved by someone.
– ∀ x [∀ y Animal(y) ⇒ Loves(x, y)] ⇒ [∃ y Loves(y, x)]
• Anyone who kills an animal is loved by no one.
– ∀ x [∃ z Animal(z) ∧ Kills(x, z)] ⇒ [∀ y ¬Loves(y, x)]
• Jack loves all animals.
– ∀ x Animal(x) ⇒ Loves(Jack, x)
• Either Jack or Curiosity killed the cat, who is named Tuna.
– Kills(Jack, Tuna) ∨ Kills(Curiosity, Tuna)
• Other facts
– Cat(Tuna)
– ∀ x Cat(x) ⇒ Animal(x)
• Did Curiosity kill the cat?
– Kills(Curiosity, Tuna)
– To prove using resolution ¬ Kills(Curiosity, Tuna)
Example 2
• ∀ x [∀ y Animal(y) ⇒ Loves(x, y)] ⇒ [∃ y Loves(y, x)]
– Animal(F(x)) ∨ Loves(G(x), x)
– ¬Loves(x, F(x)) ∨ Loves(G(x), x)
• ∀ x [∃ z Animal(z) ∧ Kills(x, z)] ⇒ [∀ y ¬Loves(y, x)]
– ¬Loves(y, x) ∨ ¬Animal(z) ∨ ¬Kills(x, z)
• ∀ x Animal(x) ⇒ Loves(Jack, x)
– ¬Animal(x) ∨ Loves(Jack, x)
• Kills(Jack, Tuna) ∨ Kills(Curiosity, Tuna)
• Cat(Tuna)
• ∀ x Cat(x) ⇒ Animal(x)
– ¬Cat(x) ∨ Animal(x)
• ¬ Kills(Curiosity, Tuna)
Figure 9.12 Example 2
(p.349)
1. Animal(F(x)) ∨ Loves(G(x), x) 9. (6,7) Animal(Tuna)
2. ¬Loves(x, F(x)) ∨ Loves(G(x), x) 10. (5,8) Kills(Jack, Tuna)
3. ¬Loves(y, x) ∨ ¬Animal(z) ∨ ¬Kills(x, z) 11. (9,3) ¬Loves(y, x) ∨ ¬Kills(x, Tuna)
4. ¬Animal(x) ∨ Loves(Jack, x) 12. (11,10) ¬Loves(y, Jack)
5. Kills(Jack, Tuna) ∨ Kills(Curiosity, Tuna) 13. (2,4) ¬Animal(F(x)) ∨ Loves(G(Jack), Jack)
6. Cat(Tuna) 14. (13,1) Loves(G(Jack), Jack)
7. ¬Cat(x) ∨ Animal(x) 15. (12,14) NIL
8. ¬ Kills(Curiosity, Tuna)
Discussion
