INFERENCE IN FIRST-ORDER LOGIC CHAPTER 9 Chapter 9 1
Inference in first-order logic Chapter 9 Chapter 9 1
Outline Reducing first-order inference to propositional inference ◇Unification Generalized Modus Ponens Forward and backward chaining ◇Logic programming ◇Resolution Chapter9 2
Outline ♦ Reducing first-order inference to propositional inference ♦ Unification ♦ Generalized Modus Ponens ♦ Forward and backward chaining ♦ Logic programming ♦ Resolution Chapter 9 2
A brief history of reasoning 450B.C. Stoics propositional logic,inference (maybe) 322B.C. Aristotle 'syllogisms"(inference rules),quantifiers 1565 Cardano probability theory(propositional logic uncertainty) 1847 Boole propositional logic (again) 1879 Frege first-order logic 1922 Wittgenstein proof by truth tables 1930 Godel 3complete algorithm for FOL 1930 Herbrand complete algorithm for FOL (reduce to propositional) 1931 Godel complete algorithm for arithmetic 1960 Davis/Putnam "practical"algorithm for propositional logic 1965 Robinson practical"algorithm for FOL-resolution Chapter 9 3
A brief history of reasoning 450b.c. Stoics propositional logic, inference (maybe) 322b.c. Aristotle “syllogisms” (inference rules), quantifiers 1565 Cardano probability theory (propositional logic + uncertainty) 1847 Boole propositional logic (again) 1879 Frege first-order logic 1922 Wittgenstein proof by truth tables 1930 G¨odel ∃ complete algorithm for FOL 1930 Herbrand complete algorithm for FOL (reduce to propositional) 1931 G¨odel ¬∃ complete algorithm for arithmetic 1960 Davis/Putnam “practical” algorithm for propositional logic 1965 Robinson “practical” algorithm for FOL—resolution Chapter 9 3
Universal instantiation (UI) Every instantiation of a universally quantified sentence is entailed by it: Vu a SUBST({v/g},a) for any variable v and ground term g Eg,Vx King(x)AGreedy(x）→Evil(x)yields King(John)A Greedy(John)Evil(John) King(Richard)A Greedy(Richard)Evil(Richard) King(Father(John))A Greedy(Father(John))Evil(Father(John)) Chapter 9 4
Universal instantiation (UI) 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) King(Richard) ∧ Greedy(Richard) ⇒ Evil(Richard) King(Father(John)) ∧ Greedy(Father(John)) ⇒ Evil(Father(John)) . . . Chapter 9 4
Existential instantiation (EI) For any sentence o,variable v,and constant symbol that does not appear elsewhere in the knowledge base: 3v a SUBST({v/k},a) E.g.,3 Crown(x)AOnHead(x,John)yields Crown(C1)A OnHead(C1,John) provided C1 is a new constant symbol,called a Skolem constant Another example:from 3 d(x)/dy=x we obtain d(e")/dy=e provided e is a new constant symbol Chapter 95
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) provided C1 is a new constant symbol, called a Skolem constant Another example: from ∃ x d(xy)/dy = xy we obtain d(ey)/dy = ey provided e is a new constant symbol Chapter 9 5