1Inference in First-Order Logic2First-Order Deduction•Want to be able to draw logically sound conclusions from aknowledge-base expressed in first-order logic.•Several styles of inference:-Forward chaining-Backward chaining-Resolution refutation•Properties of inference procedures:-Soundness: If A |− B then A |= B-Completeness: If A |= B then A |− B•Forward and backward chaining are sound and can bereasonably efficient but are incomplete.•Resolution is sound and complete for FOPC but can bevery inefficient.3Inference Rules for Quantifiers•Let SUBST(θ, α) denote the result of applying a substitutionor binding list θ to the sentence α.-SUBST({x/Tom, y,/Fred}, Uncle(x,y)) = Uncle(Tom, Fred)•Inference rules-Universal Elimination: ∀v α |− SUBST({v/g},α)for any sentence, α, variable, v, and ground term, g∀x Loves(x, FOPC) |− Loves(Ray, FOPC)-Existential Elimination: ∃v α |− SUBST({v/k},α)for any sentence, α, variable, v, and constant symbol, k,that doesn’t occur elsewhere in the KB (Skolemconstant)∃x (Owns(Mary,x) ∧ Cat(x)) |− Owns(Mary,MarysCat) ∧Cat(MarysCat)-Existential Introduction: α |- ∃v SUBST({g/v},α)for any sentence, α, variable, v, that does not occur in α,and ground term, g, that does occur in αLoves(Ray, FOPC) |− ∃x Loves(x, FOPC)4Sample Proof1) ∀x,y(Parent(x,y) ∧ Male(x) ⇒ Father(x,y))2) Parent(Tom,John)3) Male(Tom)Using Universal Elimination from 1)4) ∀y(Parent(Tom,y) ∧ Male(Tom) ⇒ Father(Tom,y))Using Universal Elimination from 4)5) Parent(Tom,John) ∧ Male(Tom) ⇒Father(Tom,John)Using And Introduction from 2) and 3)6) Parent(Tom,John) ∧ Male(Tom)Using Modes Ponens from 5) and 6)7) Father(Tom,John)5Generalized Modus Ponens•Combines three steps of “natural deduction” (UniversalElimination, And Introduction, Modus Ponens) into one.•Provides direction and simplification to the proof process forstandard inferences.•Generalized Modus Ponens:p1´, p2´, ...pn´, (p1∧ p2∧...∧pn⇒ q) |− SUBST(θ,q)where θ is a substitution such that for all iSUBST(θ,pi´)=SUBST(θ,pi)•1) ∀x,y(Parent(x,y) ∧ Male(x) ⇒ Father(x,y))2) Parent(Tom,John)3) Male(Tom)θ={x/Tom, y/John)4) Father(Tom,John)6Canonical Form•In order to utilize generalized Modus Ponens, all sentencesin the KB must be in the form of Horn sentences:∀v1,v2,...vn p1∧ p2∧...∧pm⇒ q•Also called Horn clauses, where a clause is a disjunctionof literals, because they can be rewritten as disjunctionswith at most one non-negated literal.∀v1,v2,...vn¬p1∨ ¬p2∨ ... ∨ ¬ pn∨ qIf θ is the constant False, this simplifies to∀v1,v2,...vn¬p1∨ ¬p2∨ ... ∨ ¬ pnOtherwise the sentence is called a definite clause (exactlyone non-negated literal).Single positive literals (facts) are Horn clauses with noantecedent.•Quantifiers can be dropped since all variables can beassumed to be universally quantified by default.•Many statements can be transformed into Horn clauses, butmany cannot (e.g. P(x)∨Q(x), ¬P(x))7Unification•In order to match antecedents to existing literals in the KB,need a pattern matching routine.•UNIFY(p,q) takes two atomic sentences and returns asubstitution that makes them equivalent.UNIFY(p,q)=θ where SUBST(θ,p)=SUBST(θ,q)θ is called a unifier.•ExamplesUNIFY(Parent(x,y), Parent(Tom, John)) = {x/Tom, y/John}UNIFY(Parent(Tom,x), Parent(Tom, John)) = {x/John})UNIFY(Likes(x,y), Likes(z,FOPC)) = {x/z, y/FOPC}UNIFY(Likes(Tom,y), Likes(z,FOPC)) = {z/Tom, y/FOPC}UNIFY(Likes(Tom,y), Likes(y,FOPC)) = failUNIFY(Likes(Tom,Tom), Likes(x,x)) = {x/Tom}UNIFY(Likes(Tom,Fred), Likes(x,x)) = fail8Unification(cont.)•Exact variable names used in sentences in the KB should notmatter.•But if Likes(x,FOPC) is a formula in the KB, it does not unifywith Likes(John,x) but does unify with Likes(John,y).•To avoid such conflicts, one can standardize apart one of thearguments to UNIFY to make its variables unique byrenaming them.Likes(x,FOPC) -> Likes(x1, FOPC)UNIFY(Likes(John,x),Likes(x1,FOPC)) = {x1/John, x/FOPC}•There are many possible unifiers for some atomic sentences.UNIFY(Likes(x,y),Likes(z,FOPC)) = {x/z, y/FOPC} {x/John, z/John, y/FOPC} {x/Fred, z/Fred, y/FOPC} ......UNIFY should return the most general unifier which makesthe least commitment to variable values.9Forward Chaining•Use modus ponens to always deriving all consequencesfrom new information.•Inferences cascade to draw deeper and deeperconclusions•To avoid looping and duplicated effort, must preventaddition of a sentence to the KB which is the same as onealready present.•Must determine all ways in which a rule (Horn clause) canmatch existing facts to draw new conclusions.10Forward Chaining Algorithm•A sentence is a renaming of another if it is the same except for arenaming of the variables.•The composition of two substitutions combines the variablebindings of both such that:SUBST(COMPOSE(θ1,θ2),p) = SUBST(θ2,SUBST(θ1,p))procedure FORWARD-CHAIN(KB,p)if there is a sentence in KB that is a renaming of p then returnAdd p to KBfor each ( p1^. . .^pn)q) in KB such that for some i, UNIFY(pi,p) =succeeds doFIND-AND-INFER(KB,[p1, . . ., pi1, pi+1, . .. , pn],q,)endprocedure FIND-AND-INFER(KB,premises, conclusion,)if premises = [] thenFORWARD-CHAIN(KB,SUBST(,conclusion))else for each p0in KB such that UNIFY(p0,SUBST(,FIRST(premises))) =2doFIND-AND-INFER(KB,REST( premises), conclusion, COMPOSE(,2))end11Forward Chaining ExampleAssume in KB1) Parent(x,y) ∧ Male(x) ⇒ Father(x,y)2) Father(x,y) ∧ Father(x,z) ⇒ Sibling(y,z)Add to KB3) Parent(Tom,John)Rule 1) tried but can’t “fire”Add to KB4) Male(Tom)Rule 1) now satisfied and triggered and adds:5) Father(Tom, John)Rule 2) now triggered and adds:6) Sibling(John, John) {x/Tom, y/John, z/John}Add to KB7) Parent(Tom,Fred)Rule 1) triggered again and adds:8) Father(Tom,Fred)Rule 2) triggered again and adds:9) Sibling(Fred,Fred) {x/Tom, y/Fred, z/Fred}Rule 2) triggered again and adds:10) Sibling(John, Fred) {x/Tom, y/John, z/Fred}Rule 2) triggered again and adds:11) Sibling(Fred, John) {x/Tom, y/Fred, z/John}12Problems with Forward Chaining•Inference can explode forward and may never terminate.Even(x) ⇒ Even(plus(x,2))Integer(x) ⇒