ITCS 3153 Artificial IntelligenceReasoning w/ propositional logicLogical EquivalencesSlide 4Slide 5Example of a proofSlide 7Constructing a proofMonotonicity of knowledge baseHow many inferences?ResolutionResolution Inference RuleResolution and completenessWhat about “and” clauses?CNFAn algorithm for resolutionSlide 17Example of resolutionFormal AlgorithmHorn ClausesSlide 21Slide 22Slide 23Forward ChainingSlide 25Backward ChainingITCS 3153Artificial IntelligenceLecture 11Lecture 11Logical AgentsLogical AgentsChapter 7Chapter 7Lecture 11Lecture 11Logical AgentsLogical AgentsChapter 7Chapter 7Reasoning w/ propositional logicRemember what we’ve developed so farRemember what we’ve developed so far•Logical sentencesLogical sentences•And, or, not, implies (entailment), iff (equivalence)And, or, not, implies (entailment), iff (equivalence)•Syntax vs. semanticsSyntax vs. semantics•Truth tablesTruth tables•Satisfiability, proof by contradictionSatisfiability, proof by contradictionRemember what we’ve developed so farRemember what we’ve developed so far•Logical sentencesLogical sentences•And, or, not, implies (entailment), iff (equivalence)And, or, not, implies (entailment), iff (equivalence)•Syntax vs. semanticsSyntax vs. semantics•Truth tablesTruth tables•Satisfiability, proof by contradictionSatisfiability, proof by contradictionLogical EquivalencesKnow these equivalencesKnow these equivalencesKnow these equivalencesKnow these equivalencesReasoning w/ propositional logicInference RulesInference Rules•Modus Ponens: Modus Ponens: –Whenever sentences of form Whenever sentences of form  => =>  and and  are given are giventhe sentence the sentence  can be inferred can be inferredRR11: Green => Martian: Green => MartianRR22: Green: GreenInferred: MartianInferred: MartianInference RulesInference Rules•Modus Ponens: Modus Ponens: –Whenever sentences of form Whenever sentences of form  => =>  and and  are given are giventhe sentence the sentence  can be inferred can be inferredRR11: Green => Martian: Green => MartianRR22: Green: GreenInferred: MartianInferred: MartianReasoning w/ propositional logicInference RulesInference Rules•And-EliminationAnd-Elimination–Any of conjuncts can be inferredAny of conjuncts can be inferredRR11: Martian ^ Green: Martian ^ GreenInferred: MartianInferred: MartianInferrred: GreenInferrred: GreenUse truth tables if you want to confirm inference Use truth tables if you want to confirm inference rulesrulesInference RulesInference Rules•And-EliminationAnd-Elimination–Any of conjuncts can be inferredAny of conjuncts can be inferredRR11: Martian ^ Green: Martian ^ GreenInferred: MartianInferred: MartianInferrred: GreenInferrred: GreenUse truth tables if you want to confirm inference Use truth tables if you want to confirm inference rulesrulesExample of a proof~P ~BBP?P?P?P?Example of a proof~P ~BB~PP?P?~PConstructing a proofProving Proving is like is like searchingsearching•Find sequence of logical inference rules that lead to desired Find sequence of logical inference rules that lead to desired resultresult•Note the explosion of propositionsNote the explosion of propositions–Good proof methods ignore the countless irrelevant Good proof methods ignore the countless irrelevant propositionspropositionsProving Proving is like is like searchingsearching•Find sequence of logical inference rules that lead to desired Find sequence of logical inference rules that lead to desired resultresult•Note the explosion of propositionsNote the explosion of propositions–Good proof methods ignore the countless irrelevant Good proof methods ignore the countless irrelevant propositionspropositionsMonotonicity of knowledge baseKnowledge base can only get largerKnowledge base can only get larger•Adding new sentences to knowledge base can only make it get largerAdding new sentences to knowledge base can only make it get larger–If (KB entails If (KB entails ))((KB ^ ((KB ^ ) entails ) entails ))•This is important when constructing proofsThis is important when constructing proofs–A logical conclusion drawn at one point cannot be invalidated by a A logical conclusion drawn at one point cannot be invalidated by a subsequent entailmentsubsequent entailmentKnowledge base can only get largerKnowledge base can only get larger•Adding new sentences to knowledge base can only make it get largerAdding new sentences to knowledge base can only make it get larger–If (KB entails If (KB entails ))((KB ^ ((KB ^ ) entails ) entails ))•This is important when constructing proofsThis is important when constructing proofs–A logical conclusion drawn at one point cannot be invalidated by a A logical conclusion drawn at one point cannot be invalidated by a subsequent entailmentsubsequent entailmentHow many inferences?Previous example relied on application of inference Previous example relied on application of inference rules to generate new sentencesrules to generate new sentences•When have you drawn enough inferences to prove something?When have you drawn enough inferences to prove something?–Too many make search process take longerToo many make search process take longer–Too few halt logical progression and make proof process Too few halt logical progression and make proof process incompleteincompletePrevious example relied on application of inference Previous example relied on application of inference rules to generate new sentencesrules to generate new sentences•When have you drawn enough inferences to prove something?When have you drawn enough inferences to prove something?–Too many make search process take longerToo many make search process take longer–Too few halt logical progression and make proof process Too few halt logical progression and make proof process incompleteincompleteResolutionUnit Resolution Inference RuleUnit Resolution Inference Rule•If If mm and and llii are arecomplementarycomplementaryliteralsliteralsUnit Resolution Inference RuleUnit Resolution Inference Rule•If If mm and and llii are arecomplementarycomplementaryliteralsliteralsResolution Inference RuleAlso works with clausesAlso works with clausesBut make sure each literal appears only onceBut make sure each literal appears only onceAlso works with clausesAlso works with clausesBut make sure each literal appears only