Artificial Intelligence{A brief history of reasoning}{Universal instantiation (UI)}{Existential instantiation (EI)}{UI versus EI}{Reduction to Propositional Inference}{Reduction to Propositional Inference}{Problems with Propositionalization}{Unification}{Unification}{Unification}{Unification}{Unification}{Conversion to CNF}{Conversion to CNF contd.}{Conversion to CNF contd.}{Generalized Modus Ponens (GMP)}{Soundness of GMP}{Resolution}{Soundness of Resolution}{Using Resolution}{Example Knowledge Base}{Example Knowledge Base contd.}{Example Knowledge Base contd.}{Example Knowledge Base contd.}{Example Knowledge Base contd.}{Example Knowledge Base contd.}{Example Knowledge Base contd.}{Resolution Proof: Definite Clauses}{Logic programming}{Prolog Systems}{Resolution Proof in Prolog}{Prolog Examples}Artificial IntelligenceInference in First-Order LogicReadings: Chapter 9 of Russell &Norvig.A brief history of reasoning450B.C. Stoics propositional logic, inference (maybe)322B.C. Aristotle “syllogisms” (inference rules), quantifiers1565 Cardano probability theory (propositional logic+ uncertainty)1847 Boole propositional logic (again)1879 Frege first-order logic1922 Wittgenstein proof by truth tables1930 Gödel∃ complete algorithm for FOL1930 Herbrand complete algorithm for FOL1931 Gödel¬∃ complete algorithm for arithmetic1960 Davis/Putnam “practical” algorithm for propositionallogic1965 Robinson “practical” algorithm for FOL—resolutionUniversal instantiation (UI)Every instantiation of a universally quantified sentence isentailed by it:∀ v αSUBST({v/g}, α)for any variable v and ground term gE.g., ∀ x King(x) ∧ Greedy(x) =⇒ Evil(x) yieldsKing(John) ∧ Greedy(John) =⇒ Evil(John)King(Richard) ∧ Greedy(Richard) =⇒ Evil(Richard)King(F ather(John)) ∧ Greedy(F ather(John)) =⇒ Evil(F ather(John))...Existential instantiation (EI)For any sentence α, variable v, and constant symbol kthat does not appear elsewhere in the knowledge base:∃ v αSUBST({v/k}, α)E.g., ∃ x Crown(x) ∧ OnHead(x, John) yieldsCrown(C1) ∧ OnHead(C1, John)provided C1is a new constant symbol, called a Skolemconstant.UI versus EIFrom ∀x∀y (y + x = y) we obtainy + a = yFrom ∃ x ∀y (y + x = y) we obtainy + e = yprovided e is a new constant symbol.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 existentialsentence; the new KB is not equivalent to the old, but issatisfiable iff the old KB was satisfiable.Reduction to Propositional InferenceSuppose 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 haveKing(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 areKing(John), Greedy(John), Evil(John), King(Richard) etc.Reduction to Propositional InferenceClaim: a ground sentence is entailed by new KB iffentailed by original KB.Claim: every FOL KB can be propositionalized so as topreserve entailment.Idea: propositionalize KB and query, apply resolution,return result.Problem: with function symbols, ground terms areinfinitely many, e.g.,F ather(F ather(F ather(John))).Theorem: Herbrand (1930). If a sentence α is entailedby an FOL KB, it is entailed by a finite subset of thepropositional KB.Idea: For n = 0 to ∞, create a propositional KB byinstantiating with depth-n terms see if α is entailed bythis KB.Problem: works if α is entailed, loops if α is not entailedTheorem (Turing (1936), Church (1936)) Entailment inFOL is semidecidable.Problems with PropositionalizationPropositionalization seems to generate lots of irrelevantsentences.E.g., from∀ x King(x) ∧ Greedy(x) =⇒ Evil(x)King(John)∀ y Greedy(y)Brother(Richard, John)it seems obvious that Evil(John), butpropositionalization produces lots of facts such asGreedy(Richard) that are irrelevant.In general, for one k-ary predicate and n constants,there arenkinstantiations!UnificationWe can get the inference immediately if we can find asubstitution θ such that King(x) and Greedy(x) matchKing(John) and Greedy(y). That is,θ = {x/John, y/John} worksUNIFY(α, β) = θ if αθ = βθpq θKnows(John, x) Knows(John, Jane)Knows(John, x) Knows(y, OJ)Knows(John, x) Knows(y, Mother(y))Knows(John, x) Knows(x, OJ)UnificationWe can get the inference immediately if we can find asubstitution θ such that King(x) and Greedy(x) matchKing(John) and Greedy(y). That is,θ = {x/John, y/John} worksUNIFY(α, β) = θ if αθ = βθpq θKnows(John, x) Knows(John, Jane) {x/Jane}Knows(John, x)Knows(y, OJ)Knows(John, x) Knows(y, Mother(y))Knows(John, x) Knows(x, OJ)UnificationWe can get the inference immediately if we can find asubstitution θ such that King(x) and Greedy(x) matchKing(John) and Greedy(y). That is,θ = {x/John, y/John} worksUNIFY(α, β) = θ if αθ = βθpq θ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))Knows(John, x) Knows(x, OJ)UnificationWe can get the inference immediately if we can find asubstitution θ such that King(x) and Greedy(x) matchKing(John) and Greedy(y). That is,θ = {x/John, y/John} worksUNIFY(α, β) = θ if αθ = βθpq θ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)UnificationWe can get the inference immediately if we can find asubstitution θ such that King(x) and Greedy(x) matchKing(John) and Greedy(y). That is,θ = {x/John, y/John} works.UNIFY(α, β) = θ if αθ = βθpq θ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) failStandardizing apart eliminates overlap of variables, e.g.,Knows(z17, OJ)Conversion to CNFEveryone 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)]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)]∀ x [∃ y