Inference in First Order LogicInference Rules for FOLExistential EliminationSlide 4Slide 5Resolution for FOLSlide 7Converting FOL sentences to clause formConversion procedureConversion examplesSlide 11Unification of two clausesSlide 13Slide 14Unification ExamplesMore Unification ExamplesUnification AlgorithmResolution in FOLResolution exampleResolution Refutation: a better proof strategySlide 21Refutation Resolution ProcedureExample of Automatic Theorem Proof: Did Curiosity kill the catSlide 24Slide 25Slide 26Horn ClausesLogic ProgrammingExample of Logic Programming Computing factorialsPrologControl StrategiesSlide 32Slide 33Slide 34Other issuesSlide 36Slide 371Inference in Inference in First Order LogicFirst Order LogicChapter 92Inference Rules for FOL•Inference rules for PL apply to FOL as well (Modus Ponens, And-Introduction, And-Elimination, etc.) •New (sound) inference rules for use with quantifiers: –Universal Elimination–Existential Introduction–Existential Elimination–Generalized Modus Ponens (GMP)•Resolution –Clause form (CNF in FOL)–Unification (consistent variable substitution)–Refutation resolution (proof by contradiction)3Universal Elimination (x) P(x) |-- P(c).•If (x) P(x) is true, then P(c) is true for any constant c in the domain of x, i.e.,, (x) P(x) |= P(c).•Replace all occurrences of x in the scope of x by the same ground term (a constant or a ground function).•Example: (x) eats(Ziggy, x) |-- eats(Ziggy, IceCream)Existential Introduction P(c) |-- (x) P(x)•If P(c) is true, so is (x) P(x), i.e., P(c) |= (x) P(x)•Replace all instances of the given constant symbol by the same new variable symbol. •Example eats(Ziggy, IceCream) |-- (x) eats(Ziggy, x)Existential Elimination•From (x) P(x) infer P(c), i.e., (x) P(x) |= P(c), where c is a new constant symbol, –All we know is there must be some constant that makes this true, so we can introduce a brand new one to stand in for that constant, even though we don’t know exactly what that constant refer to.–Example: (x) eats(Ziggy, x) |= eats(Ziggy, Stuff)4•Things become more complicated when there are universal quantifiers (x)(y) eats(x, y) |= (x)eats(x, Stuff) ??? (x)(y) eats(x, y) |= eats(Ziggy, Stuff) ??? –Introduce a new function food_sk(x) to stand for y because that y depends on x (x)(y) eats(x, y) |-- (x)eats(x, food_sk(x)) (x)(y) eats(x, y) |-- eats(Ziggy, food_sk(Ziggy)) –What exactly the function food_sk(.) does is unknown, except that it takes x as its argument•The process of existential elimination is called “Skolemization”, and the new, unique constants (e.g., Stuff) and functions (e.g., food_sk(.)) are called skolem constants and skolem functions5Generalized Modus Ponens (GMP)•Combines And-Introduction, Universal-Elimination, and Modus Ponens •Ex: P(c), Q(c), (x)(P(x) ^ Q(x)) => R(x) |-- R(c) P(c), Q(c) |-- P(c) ^ Q(c) (by and-introduction)(x)(P(x) ^ Q(x)) => R(x) |-- (P(c) ^ Q(c)) => R(c) (by universal-elimination)P(c) ^ Q(c), (P(c) ^ Q(c)) => R(c) |-- R(c) (by modus ponens)•All occurrences of a quantified variable must be instantiated to the same constant.P(a), Q(c), (x)(P(x) ^ Q(x)) => R(x) |-- R(c)because all occurrences of x must either instantiated to a or c which makes the modus ponens rule not applicable.6Resolution for FOL•Resolution rule operates on two clauses–A clause is a disjunction of literals (without explicit quantifiers)–Relationship between clauses in KB is conjunction•Resolution Rule for FOL:–clause C1: (l1, l2, ... li, ... ln) and clause C2: (l’1, l’2, ... l’j, ... l’m) –if li and l’j are two opposite literals (e.g., P and ~P) and their argument lists can be be made the same (unified) by a set of variable bindings {x1/y1, ... Xk/yk} where x1, ... Xk are variables and y1, ... Yk are terms, then derive a new clause (called resolvent) subst((l1, l2, ... ln, l’1, l’2, ... l’m), where function subst(expression, returns a new expression by applying all variable bindings in  to the original expression7We need answers to the following questions •How to convert FOL sentences to clause form (especially how to remove quantifiers)•How to unify two argument lists, i.e., how to find their most general unifier (mgu) •How to determine which two clauses in KB should be resolved next (among all resolvable pairs of clauses) and how to determine a proof is completed8Converting FOL sentences to clause form•Clauses are quantifier free CNF of FOL sentences•Basic ideas–How to handle quantifiers •Careful on quantifiers with preceding negations (explicit or implicit)~x P(x) is really x ~P(x) (x P(x)) => (y Q(y)) ~(x P(x)) v (y Q(y)) x ~P(x) v y Q(y) •Eliminate true existential quantifier by Skolemization•For true universally quantified variables, treat them as such without quantifiers–How to convert to CNF (similar to PL but need to work with quantifiers)9Conversion procedurestep 1: remove all “=>” and “<=>” operators(using P => Q ~P v Q and P <=> Q P => Q ^ Q => P)step 2: move all negation signs to individual predicates (using de Morgan’s law)step 3: remove all existential quantifiers y case 1: y is not in the scope of any universally quantified variable, then replace all occurrences of y by a skolem constant case 2: if y is in scope of universally quantified variables x1, ... xi, then replace all occurrences of y by a skolem function that takes x1, ... Xi as its argumentsstep 4: remove all universal quantifiers x (with the understanding that all remaining variables are universally quantified)step 5: convert the sentence into CNF (using distribution law, etc) step 6: use parenthesis to separate all disjunctions, then drop all v’s and ^’s10Conversion examplesx (P(x) ^ Q(x) => R(x))x ~(P(x) ^ Q(x)) v R(x) (by step 1) x ~P(x) v ~Q(x) v R(x) (by step 2)~P(x) v ~Q(x) v R(x) (by step 4)(~P(x), ~Q(x), R(x)) (by step 6)y rose(y) ^ yellow(y) rose(c) ^ yellow(c) (where c is a skolem constant)(rose(c)), (yellow(c))11Conversion examplesx [person(x) => y (person(y) ^ father(y, x))]x [~person(x) v y (person(y) ^ father(y, x))] (by step 1)x [~person(x) v (person(f_sk(x)) ^ father(f_sk(x), x))] (by step 3) ~person(x) v