1CS 1571 Intro to AIM. HauskrechtCS 1571 Introduction to AILecture 19Milos [email protected] Sennott SquareInference in first-order logic CS 1571 Intro to AIM. HauskrechtLogical inference in FOLLogical inference problem:• Given a knowledge base KB (a set of sentences) and a sentence , does the KB semantically entail ?In other words: In all interpretations in which sentences in the KB are true, is also true?Logical inference problem in the first-order logic is undecidable !!!. No procedure that can decide the entailment for all possible input sentencesin a finite number of steps.α=|KB?ααα2CS 1571 Intro to AIM. HauskrechtLogical inference problem in the Propositional logicComputational procedures that answer: Three approaches:• Truth-table approach• Inference rules• Conversion to the inverse SAT problem– Resolution-refutation α=|KB?CS 1571 Intro to AIM. HauskrechtInference rules• Inference rules from the propositional logic:– Modus ponens– Resolution– and others: And-introduction, And-elimination, Or-introduction, Negation elimination• Additional inference rules are needed for sentences with quantifiers and variables– Must involve variable substitutionsBABA ,⇒CACBBA∨∨¬∨ ,3CS 1571 Intro to AIM. HauskrechtVariable substitutions• Variables in the sentences can be substituted with terms.(terms = constants, variables, functions)• Substitution:– Is represented by a mapping from variables to terms– Application of the substitution to sentences},/,/{2211Ktxtx),()),(},/,/({ PamSamLikesyxLikesPamySamxSUBST=))(,()),()},(/,/({JohnfatherofzLikesyxLikesJohnfatherofyzxSUBST=CS 1571 Intro to AIM. HauskrechtInference rules for quantifiers• Universal elimination– substitutes a variable with a constant symbol• Existential elimination.– Substitutes a variable with a constant symbol that does not appear elsewhere in the KB)()(axxφφ∃)()(axxφφ∀a- is a constant symbol),( IceCreamxLikesx∀ ),( IceCreamBenLikes),( VictimxKillx∃),( VictimMurdererKill4CS 1571 Intro to AIM. HauskrechtInference rules for quantifiers• Universal instantiation (introduction)– Introduces a universal variable which does not affect or its assumptions• Existential instantiation (introduction)– Substitutes a ground term in the sentence with a variable and an existential statement)()(xxaφφ∃φφx∀x – is not free in φa – is a ground term inx – is not free in φφφ),( IceCreamxLikesx∃),( IceCreamBenLikes),( JaneAmySister),( JaneAmySisterx∀CS 1571 Intro to AIM. HauskrechtUnification• Problem in inference: Universal elimination gives many opportunities for substituting variables with ground terms• Solution: Try substitutions that may help– Use substitutions of “similar” sentences in KB • Unification – takes two similar sentences and computes the substitution that makes them look the same, if it exists),(), s.t. ),( qSUBSTpSUBST( σqpUNIFYσσ==)()(axxφφ∀a- is a constant symbol5CS 1571 Intro to AIM. HauskrechtUnification. Examples.• Unification:• Examples:}/{)),(),,(( JanexJaneJohnKnowsxJohnKnowsUNIFY=}/,/{)),(),,(( JohnyAnnxAnnyKnowsxJohnKnowsUNIFY=failElizabethxKnowsxJohnKnowsUNIFY=)),(),,((}/),(/{ )))(,(),,((JohnyJohnMotherOfxyMotherOfyKnowsxJohnKnowsUNIFY=),(), s.t. ),( qSUBSTpSUBST( σqpUNIFYσσ==CS 1571 Intro to AIM. HauskrechtGeneralized inference rules.• Use substitutions that let us make inferencesExample: Modus Ponens• If there exists a substitution such that• Substitution that satisfies the generalized inference rule can be build via unification process• Advantage of the generalized rules: they are focused– only substitutions that allow the inferences to proceed ),(',',',2121BSUBSTAAABAAAnnσKK ⇒∧∧)',(),(iiASUBSTASUBSTσσ=σfor all i=1,2, n6CS 1571 Intro to AIM. HauskrechtResolution inference rule• Recall: Resolution inference rule is sound and complete (refutation-complete) for the propositional logic and CNF• Generalized resolution rule is sound and refutation completefor the first-order logic and CNF w/o equalities (if unsatisfiablethe resolution will find the contradiction)CBCABA∨∨¬∨ ,),(,1111112121njjkiinkSUBSTψψψψφφφφσψψψφφφKKKKKK+−+−∨∨∨∨∨∨∨∨∨∨∨∨failUNIFYji≠¬= ),(ψφσExample:?)()(),()( ySJohnQxQxP ∨¬∨CS 1571 Intro to AIM. HauskrechtResolution inference rule• Recall: Resolution inference rule is sound and complete (refutation-complete) for the propositional logic and CNF• Generalized resolution rule is sound and refutation completefor the first-order logic and CNF w/o equalities (if unsatisfiablethe resolution will find the contradiction)CBCABA∨∨¬∨ ,),(,1111112121njjkiinkSUBSTψψψψφφφφσψψψφφφKKKKKK+−+−∨∨∨∨∨∨∨∨∨∨∨∨failUNIFYji≠¬= ),(ψφσExample:)()()()(),()(ySJohnPySJohnQxQxP∨∨¬∨7CS 1571 Intro to AIM. HauskrechtInference with resolution rule• Proof by refutation:– Prove that is unsatisfiable– resolution is refutation-complete• Main procedure (steps):1. Convert to CNF with ground terms and universal variables only2. Apply repeatedly the resolution rule while keeping track and consistency of substitutions3. Stop when empty set (contradiction) is derived or no more new resolvents (conclusions) followα¬,KBα¬,KBCS 1571 Intro to AIM. HauskrechtConversion to CNF1. Eliminate implications, equivalences2. Move negations inside (DeMorgan’s Laws, double negation)3. Standardize variables (rename duplicate variables)4. Move all quantifiers left (no invalid capture possible ))()( qpqp ∨¬→⇒qpqp¬∨¬→∧¬ )(qpqp¬∧¬→∨¬ )(pxpx¬∃→¬∀pxpx¬∀→¬∃pp→¬¬))(())(())(())(( yQyxPxxQxxPx∃∨∀→∃∨∀)()())(())(( yQxPyxyQyxPx ∨∃∀→∃∨∀8CS 1571 Intro to AIM. HauskrechtConversion to CNF5. Skolemization (removal of existential quantifiers through elimination)• If no universal quantifier occurs before the existential quantifier, replace the variable with a new constant symbol• If a universal quantifier precede the existential quantifier replace the variable with a function of the “universal” variable))(()()()( xFQxPxyQxPyx ∨∀→∨∃∀)()()()( BQAPyQAPy ∨→∨∃)( xF- called Skolem function- a special functionCS 1571 Intro to AIM. HauskrechtConversion to CNF6. Drop universal quantifiers (all variables are universally quantified)7.