1CS 1571 Intro to AIM. HauskrechtCS 1571 Introduction to AILecture 16Milos [email protected] Sennott SquarePropositional logic. CS 1571 Intro to AIM. HauskrechtLogical inference problemLogical inference problem:• Given:– a knowledge base KB (a set of sentences) and – a sentence (called a theorem), • Does a KB semantically entail ?In other words: In all interpretations in which sentences in the KB are true, is also true?Approaches:• Truth-table approach• Inference rules• Conversion to SAT – Resolution refutation α=|KB?ααα2CS 1571 Intro to AIM. HauskrechtαTruth-table approachProblem:• We need to check all possible interpretations for which the KB is true (models of KB) whether is true for each of themTruth tables:• enumerate truth values of sentences for all possible interpretations (assignments of True/False to propositional symbols) and checkExample: αPQQP ∨TrueTrue TrueTrue FalseFalseFalse False FalseTrueTrueTrueTrueFalseFalseFalseα=|KB?QP⇔TrueFalseFalseTrueKBQQP∧¬∨ )(CS 1571 Intro to AIM. HauskrechtInference rules approach.Motivation: we do not want to blindly generate and check all interpretations !!!Inference rules:•Represent sound inference patterns repeated in inferences• Application of many inference rules allows us to infer new sound conclusions and hence prove theorems• An example of an inference rule: Modus ponensBABA ,⇒premiseconclusion3CS 1571 Intro to AIM. HauskrechtExample. Inference rules approach.KB: Theorem:1. 2.3.4. From 1 and And-elim5. From 2,4 and Modus ponens6. From 1 and And-elim7. From 5,6 and And-introduction8. From 7,3 and Modus ponensQP ∧RP ⇒SRQ ⇒∧ )(SPRQ)( RQ ∧QP ∧RP ⇒SRQ ⇒∧)(SSProved:CS 1571 Intro to AIM. HauskrechtExample. Inference rules approach.KB: Theorem:1. 2.3.4. From 1 and And-elim5. From 2,4 and Modus ponens6. From 1 and And-elim7. From 5,6 and And-introduction8. From 7,3 and Modus ponensQP ∧RP ⇒SRQ ⇒∧ )(SPRQ)( RQ ∧QP ∧RP ⇒SRQ ⇒∧)(SSProved:Nondeterministic steps4CS 1571 Intro to AIM. HauskrechtLogic inferences and searchInference rule method as a search problem:• State: a set of sentences that are known to be true• Initial state: a set of sentences in the KB• Operators: applications of inference rules – Allow us to add new sound sentences to old ones• Goal state: a theorem is derived from KB Logic inference: • Proof: A sequence of sentences that are immediate consequences of applied inference rules• Theorem proving: process of finding a proof of theoremαCS 1571 Intro to AIM. HauskrechtSatisfiability (SAT) problemDetermine whether a sentence in the conjunctive normal form (CNF) is satisfiable (I.e. can evaluate to true)It is an instance of a constraint satisfaction problem:• Variables:– Propositional symbols (P, R, T, S)– Values: True, False• Constraints:– Every conjunct must evaluate to true, at least one of the literals must evaluate to true• All techniques developed for CSPs can be applied to solve the logical inference problem. Why?K)()()( TQPSRPRQP¬∨∨¬∧∨¬∨¬∧¬∨∨5CS 1571 Intro to AIM. HauskrechtInference problem and satisfiabilityInference problem:• we want to show that the sentence is entailed by KB Satisfiability:• The sentence is satisfiable if there is some assignment (interpretation) under which the sentence evaluates to trueConnection:Consequences: • inference problem is NP-complete• programs for solving the SAT problem can be used to solve the inference problem (Simulated-annealing, WALKSAT)αα=|KBif and only if )(α¬∧KBis unsatisfiableCS 1571 Intro to AIM. HauskrechtSatisfiability (SAT) problemDetermine whether a sentence in the conjunctive normal form (CNF) is satisfiable (i.e. can evaluate to true)It is an instance of a constraint satisfaction problem:• Variables:– Propositional symbols (P, R, T, S)– Values: True, False• Constraints:– Every conjunct must evaluate to true, at least one of the literals must evaluate to true• Why is this important? All techniques developed for CSPscan be applied to solve the logical inference problem !!K)()()( TQPSRPRQP¬∨∨¬∧∨¬∨¬∧¬∨∨6CS 1571 Intro to AIM. HauskrechtResolution algorithmAlgorithm: 1. Convert KB to the CNF form;2. Apply iteratively the resolution rule starting from (in the CNF form)3. Stop when:– Contradiction (empty clause) is reached:•• proves the entailment.– No more new sentences can be derived • Rejects (disproves) the entailment.α¬,KBOAA →¬,CS 1571 Intro to AIM. HauskrechtExample. Resolution.KB: Theorem:])[()()( SRQRPQP ⇒∧∧⇒∧∧S7CS 1571 Intro to AIM. HauskrechtExample. Resolution.KB: Theorem:Step 1. convert KB to CNF: •••KB:Step 2. Negate the theorem to prove it via refutationStep 3. Run resolution on the set of clauses QP ∧SPQ])[()()( SRQRPQP ⇒∧∧⇒∧∧SQP∧RP ⇒)( RP ∨¬SRQ ⇒∧ )( )( SRQ ∨¬∨¬)( RP ∨¬)( SRQ ∨¬∨¬S¬PQ)( RP ∨¬)( SRQ ∨¬∨¬S¬CS 1571 Intro to AIM. HauskrechtExample. Resolution.KB: Theorem:S])[()()( SRQRPQP ⇒∧∧⇒∧∧S{}PQ)( RP ∨¬)( SRQ ∨¬∨¬S¬R)( SR ∨¬ContradictionSProved:8CS 1571 Intro to AIM. HauskrechtKB in restricted forms• If the sentences in the KB are restricted to some special forms other sound inference rules may become completeExample:• Horn form (Horn normal form)• Modus ponens:– is the “universal “(complete) rule for the sentences in the Horn form)()( DCABA ∨¬∨¬∧¬∨))(()( DCAAB ⇒∧∧⇒Can be written also as:BABA ,⇒BAAABAAAkkKK ,,,2121⇒∧∧∧CS 1571 Intro to AIM. HauskrechtKB in Horn form• Horn form: a clause with at most one positive literal• Not all sentences in propositional logic can be converted into the Horn form• KB in Horn normal form:– Two types of propositional statements:• Implications: called rules • Propositional symbols: facts• Application of the modus ponens:– Infers new facts from previous facts)()( DCABA ∨¬∨¬∧¬∨BABA ,⇒)( AB ⇒B9CS 1571 Intro to AIM. HauskrechtForward and backward chainingTwo inference procedures based on modus ponens for Horn KBs:• Forward chainingIdea: Whenever the premises of a rule are satisfied, infer the conclusion. Continue with rules that became satisfied.• Backward chaining (goal reduction)Idea: To prove the fact that appears in the conclusion of a rule prove the premises of the rule. Continue