1Inference in first-order logicChapter 9Outline• Reducing first-order inference to propositional inference• Unification• Generalized Modus Ponens• Forward chaining• Backward chaining• Resolution2Inference with Quantifiers• Universal Instantiation: – Given ∀X person(X) ⇒ likes(X, sun)– Infer person(john) ⇒ likes(john,sun) • Existential Instantiation:– Given ∃x likes(x, chocolate)– Infer: likes(S1, chocolate)– S1 is a “Skolem Constant” that is not found anywhere else in the KB and refers to (one of) the individuals that likes sun.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))...3Existential 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 C1is a new constant symbol, called a Skolem constantReduction 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 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 areKing(John), Greedy(John), Evil(John), King(Richard), etc.4Reduction contd.• 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, there are infinitely many ground terms,– e.g., Father(Father(Father(John)))Reduction contd.Theorem: Herbrand (1930). If a sentence α is entailed by an FOL KB, it is entailed by a finite subset of the propositionalized KBIdea: For n = 0 to ∞ docreate a propositional KB by instantiating with depth-$n$ termssee if α is entailed by this KBProblem: works if α is entailed, loops if α is not entailedTheorem: Turing (1936), Church (1936) Entailment for FOL is semidecidable (algorithms exist that say yes to every entailed sentence, but no algorithm exists that also says no to every nonentailed sentence.)5Problems 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·nkinstantiations.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) Knows(John,x) Knows(y,OJ) Knows(John,x) Knows(y,Mother(y))Knows(John,x) Knows(x,OJ) • Standardizing apart eliminates overlap of variables, e.g., Knows(z17,OJ)6Unification• 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) Knows(John,x) Knows(y,Mother(y))Knows(John,x) Knows(x,OJ) • Standardizing apart eliminates overlap of variables, e.g., Knows(z17,OJ)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))Knows(John,x) Knows(x,OJ) • Standardizing apart eliminates overlap of variables, e.g., Knows(z17,OJ)7Unification• 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) • Standardizing apart eliminates overlap of variables, e.g., Knows(z17,OJ)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)8More on Standardizing apart• knows(john,X).• knows(X,elizabeth).• These ought to unify, since john knows everyone, and everyone knows elizabeth. •Rename variables to avoid such name clashes Note:all X p(X) == all Y p(Y)All X (p(X) ^ q(X)) == All X p(X) ^ All Y p(Y)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.• There is a single most general unifier (MGU) that is unique up to renaming of variables.MGU = { y/John, x/z }9Generalized Modus Ponens• This is a general inference rule for FOL that does not require instantiation • GMP “lifts” MP from propositional to first-order logic• Key advantage of lifted inference rules over propositionalization is that they make only substitutions which are required to allow particular inferences to proceedExample 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.• Prove that Col. West is a criminal10Example knowledge base contd.... it is a crime for an American to sell weapons to hostile