ITCS 3153 Artificial IntelligenceForward ChainingLifting forward chainingExampleSlide 5Slide 6Forward-chainingFirst iteration of forward chainingSlide 9Second iteration of forward chainingAnalyze this algorithmProving completenessComplexit of this algorithmPattern matchingIncremental forward chainingIrrelevant factsMagic SetBackward ChainingResolutionFirst-order CNFSlide 21Slide 22Slide 23Slide 24Resolution inference ruleSlide 26ITCS 3153Artificial IntelligenceLecture 15Lecture 15First-Order LogicFirst-Order LogicChapter 9Chapter 9Lecture 15Lecture 15First-Order LogicFirst-Order LogicChapter 9Chapter 9Forward ChainingRemember this from propositional logic?Remember this from propositional logic?•Start with atomic sentences in KBStart with atomic sentences in KB•Apply Modus PonensApply Modus Ponens–add new sentences to KBadd new sentences to KB–discontinue when no new sentencesdiscontinue when no new sentences•Hopefully find the sentence you are looking for in the Hopefully find the sentence you are looking for in the generated sentencesgenerated sentencesRemember this from propositional logic?Remember this from propositional logic?•Start with atomic sentences in KBStart with atomic sentences in KB•Apply Modus PonensApply Modus Ponens–add new sentences to KBadd new sentences to KB–discontinue when no new sentencesdiscontinue when no new sentences•Hopefully find the sentence you are looking for in the Hopefully find the sentence you are looking for in the generated sentencesgenerated sentencesLifting forward chainingFirst-order definite clausesFirst-order definite clauses•all sentences are defined this way to simplify processingall sentences are defined this way to simplify processing–disjunction of literals with exactly one positivedisjunction of literals with exactly one positive–clause is either atomic or an implication whose antecedent clause is either atomic or an implication whose antecedent is a conjunction of positive literals and whose consequent is a conjunction of positive literals and whose consequent is a single positive literalis a single positive literalFirst-order definite clausesFirst-order definite clauses•all sentences are defined this way to simplify processingall sentences are defined this way to simplify processing–disjunction of literals with exactly one positivedisjunction of literals with exactly one positive–clause is either atomic or an implication whose antecedent clause is either atomic or an implication whose antecedent is a conjunction of positive literals and whose consequent is a conjunction of positive literals and whose consequent is a single positive literalis a single positive literalExample•The law says it is a crime for an American to sell weapons to The law says it is a crime for an American to sell weapons to hostile nations. The country Nono, an enemy of America, hostile nations. The country Nono, an enemy of America, has some missiles, and all of its missles were sold to it by has some missiles, and all of its missles were sold to it by Colonel West, who is AmericanColonel West, who is American•We will prove West is a criminalWe will prove West is a criminal•The law says it is a crime for an American to sell weapons to The law says it is a crime for an American to sell weapons to hostile nations. The country Nono, an enemy of America, hostile nations. The country Nono, an enemy of America, has some missiles, and all of its missles were sold to it by has some missiles, and all of its missles were sold to it by Colonel West, who is AmericanColonel West, who is American•We will prove West is a criminalWe will prove West is a criminalExample•It is a crime for an American to sell weapons to hostile nationsIt is a crime for an American to sell weapons to hostile nations•Nono… has some misslesNono… has some missles–Owns (Nono, M1)Owns (Nono, M1)–Missile (M1)Missile (M1)•All of its missiles were sold to it by Colonel WestAll of its missiles were sold to it by Colonel West•It is a crime for an American to sell weapons to hostile nationsIt is a crime for an American to sell weapons to hostile nations•Nono… has some misslesNono… has some missles–Owns (Nono, M1)Owns (Nono, M1)–Missile (M1)Missile (M1)•All of its missiles were sold to it by Colonel WestAll of its missiles were sold to it by Colonel WestExample•We also need to know that missiles are weaponsWe also need to know that missiles are weapons•and we must know that an enemy of America counts as and we must know that an enemy of America counts as “hostile”“hostile”•““West, who is American”West, who is American”•The country Nono, an enemy of AmericaThe country Nono, an enemy of America•We also need to know that missiles are weaponsWe also need to know that missiles are weapons•and we must know that an enemy of America counts as and we must know that an enemy of America counts as “hostile”“hostile”•““West, who is American”West, who is American”•The country Nono, an enemy of AmericaThe country Nono, an enemy of AmericaForward-chainingStarting from the factsStarting from the facts•find all rules with satisfied premisesfind all rules with satisfied premises•add their conclusions to known factsadd their conclusions to known facts•repeat untilrepeat until–query is answeredquery is answered–no new facts are addedno new facts are addedStarting from the factsStarting from the facts•find all rules with satisfied premisesfind all rules with satisfied premises•add their conclusions to known factsadd their conclusions to known facts•repeat untilrepeat until–query is answeredquery is answered–no new facts are addedno new facts are addedFirst iteration of forward chainingLook at the implication sentences firstLook at the implication sentences first•must satisfy unknown premisesmust satisfy unknown premises•We can satisfy this ruleWe can satisfy this rule–by substituting {x/M1} by substituting {x/M1} –and adding Sells(West, M1, Nono) to KBand adding Sells(West, M1, Nono) to KBLook at the implication sentences firstLook at the implication sentences first•must satisfy unknown premisesmust satisfy unknown premises•We can satisfy this ruleWe can satisfy this rule–by substituting {x/M1} by substituting {x/M1} –and adding Sells(West, M1, Nono) to KBand adding Sells(West, M1, Nono) to KBFirst iteration of forward chaining•We can satisfyWe can satisfy–with