Unformatted text preview:

1CS 1571 Intro to AIM. HauskrechtCS 1571 Introduction to AILecture 15Milos [email protected] Sennott SquarePropositional logic CS 1571 Intro to AIM. HauskrechtAnnouncementsMidterm exam: • Wednesday, October 25, 2006Course web page:http://www.cs.pitt.edu/~milos/courses/cs1571/2CS 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?Question: Is there a procedure (program) that can decide this problem in a finite number of steps?Answer: Yes. Logical inference problem for the propositional logic is decidable.α=|KB?αααCS 1571 Intro to AIM. HauskrechtSolving logical inference problemIn the following:How to design the procedure that answers: Three approaches:• Truth-table approach• Inference rules• Conversion to the inverse SAT problem– Resolution-refutation α=|KB?3CS 1571 Intro to AIM. HauskrechtTruth-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 table:• enumerates truth values of sentences for all possible interpretations (assignments of True/False values to propositional symbols)Example: αPQQP ∨QQP∧¬∨ )(TrueTrue TrueTrue FalseFalseFalse False FalseTrueTrueTrueTrueFalseFalseFalseα=|KB?QP⇔TrueFalseFalseTrueKBαCS 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 table:• enumerates truth values of sentences for all possible interpretations (assignments of True/False to propositional symbols)Example: αPQQP ∨TrueTrue TrueTrue FalseFalseFalse False FalseTrueTrueTrueTrueFalseFalseFalseα=|KB?QP⇔TrueFalseFalseTrueKBQQP∧¬∨ )(4CS 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 table:• enumerates truth values of sentences for all possible interpretations (assignments of True/False to propositional symbols)Example: αPQQP ∨TrueTrue TrueTrue FalseFalseFalse False FalseTrueTrueTrueTrueFalseFalseFalseα=|KB?QP⇔TrueFalseFalseTrueKBQQP∧¬∨ )(CS 1571 Intro to AIM. HauskrechtInference rules approach.Problem with the truth table approach:• the truth table is exponential in the number of propositional symbols (we checked all assignments)• KB is true on only a smaller subsetHow to make the process more efficient?Solution: check only entries for which KB is True. This is the idea behind the inference rules approachInference rules:• Represent sound inference patterns repeated in inferences• Can be used to generate new (sound) sentences from the existing onesα=|KB?5CS 1571 Intro to AIM. HauskrechtInference rules for logic• Modus ponens• If both sentences in the premise are true then conclusion is true.• The modus ponens inference rule is sound.– We can prove this through the truth table.BABA ,⇒premiseconclusionBA ⇒ABFalse False TrueFalseTrueTrueTrueTrueTrueFalse FalseTrueCS 1571 Intro to AIM. HauskrechtExample. Inference rules approach.KB: Theorem:1. 2.3.QP ∧RP ⇒SRQ ⇒∧ )(QP ∧RP ⇒SRQ ⇒∧)(S6CS 1571 Intro to AIM. HauskrechtExample. Inference rules approach.KB: Theorem:1. 2.3.4. From 1 and And-elimQP ∧RP ⇒SRQ ⇒∧ )(PQP ∧RP ⇒SRQ ⇒∧)(SinAAAA∧∧21CS 1571 Intro to AIM. HauskrechtExample. Inference rules approach.KB: Theorem:1. 2.3.4. 5. From 2,4 and Modus ponensQP ∧RP ⇒SRQ ⇒∧ )(PRQP ∧RP ⇒SRQ ⇒∧)(SBABA,⇒7CS 1571 Intro to AIM. HauskrechtExample. Inference rules approach.KB: Theorem:1. 2.3.4. 5. 6. From 1 and And-elimQP ∧RP ⇒SRQ ⇒∧ )(PRQQP ∧RP ⇒SRQ ⇒∧)(SinAAAA∧∧21CS 1571 Intro to AIM. HauskrechtExample. Inference rules approach.KB: Theorem:1. 2.3.4. 5. 6.7. From 5,6 and And-introductionQP ∧RP ⇒SRQ ⇒∧ )(PRQ)( RQ ∧QP ∧RP ⇒SRQ ⇒∧)(SnnAAAAAA∧∧2121,,8CS 1571 Intro to AIM. HauskrechtExample. Inference rules approach.KB: Theorem:1. 2.3.4. 5. 6.7.8. From 7,3 and Modus ponensQP ∧RP ⇒SRQ ⇒∧ )(SPRQ)( RQ ∧QP ∧RP ⇒SRQ ⇒∧)(SSProved:BABA ,⇒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:9CS 1571 Intro to AIM. HauskrechtLogic inferences and search• To show that theorem holds for a KB – we may need to apply a number of sound inference rulesProblem: many possible rules to can be applied nextLooks familiar?This is an instance of a search problem: Truth table method (from the search perspective):– blind enumeration and checkingαQPQP ,⇒SRSR ,⇒QP ⇒SR ⇒RP…?CS 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α10CS 1571 Intro to AIM. HauskrechtNormal formsSentences in the propositional logic can be transformed into one of the normal forms. This can simplify the inferences.Normal forms used: Conjunctive normal form (CNF)• conjunction of clauses (clauses include disjunctions of literals)Disjunctive normal form (DNF)• Disjunction of terms (terms include conjunction of literals))()( DCABA ∨¬∨¬∧∨)()()( DCCABA¬∧∨∧¬∨¬∧CS 1571 Intro to AIM. HauskrechtConversion to a CNFAssume:1. Eliminate2. Reduce the scope of signs through DeMorgan Laws and double negation3. Convert to CNF using the associative and distributive lawsand)()( ACBA ∨¬∨∨¬¬)()( ACBA ∨¬∨¬∧)()( ACBA ⇒∨⇒¬)()( ACBACA ∨¬∨¬∧∨¬∨)()( ACBCA ∨¬∨¬∧¬∨⇔⇒,11CS 1571 Intro to AIM. HauskrechtSatisfiability (SAT) problemDetermine whether a


View Full Document

Pitt CS 1571 - Introduction to Lecture 15

Download Introduction to Lecture 15
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Introduction to Lecture 15 and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Introduction to Lecture 15 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?