ITCS 3153 Artificial IntelligenceInference in first-order logicSearch and forward chainingSlide 4Slide 5Search and backward chainingSlide 7Slide 8Backward/forward chainingInference with resolutionResolutionSlide 12Slide 13ExampleResolution exampleSlide 16Slide 17Theorem proversPractical theorem proversSlide 20Statistical Learning MethodsRational agentsHow early will my son be born?Slide 24Function ApproximatorSlightly more complicatedMappingsNeural NetworksSlide 29ITCS 3153Artificial IntelligenceLecture 17Lecture 17First-Order LogicFirst-Order LogicChapter 9Chapter 9Lecture 17Lecture 17First-Order LogicFirst-Order LogicChapter 9Chapter 9Inference in first-order logicOur goal is to prove that KB entails a fact, Our goal is to prove that KB entails a fact, •We use logical inferenceWe use logical inferenceForward chainingForward chainingBackward chainingBackward chainingResolutionResolutionAll three logical inference systems rely on search All three logical inference systems rely on search to find a sequence of actions that derive the empty to find a sequence of actions that derive the empty clauseclauseOur goal is to prove that KB entails a fact, Our goal is to prove that KB entails a fact, •We use logical inferenceWe use logical inferenceForward chainingForward chainingBackward chainingBackward chainingResolutionResolutionAll three logical inference systems rely on search All three logical inference systems rely on search to find a sequence of actions that derive the empty to find a sequence of actions that derive the empty clauseclauseSearch and forward chainingStart with KB full of first-order definite clausesStart with KB full of first-order definite clauses•Disjunction of literals with exactly one positiveDisjunction of literals with exactly one positive–Equivalent to implication with conjunction of positive Equivalent to implication with conjunction of positive literals on left (antecedent / body / premise) and one literals on left (antecedent / body / premise) and one positive literal on right (consequent / head / conclusion)positive literal on right (consequent / head / conclusion)–Propositional logic used Horn clauses, which permit zero Propositional logic used Horn clauses, which permit zero oror one to be positive one to be positive•Look for rules with premises that are satisfied (use Look for rules with premises that are satisfied (use substitution to make matches) and add conclusions to KBsubstitution to make matches) and add conclusions to KBStart with KB full of first-order definite clausesStart with KB full of first-order definite clauses•Disjunction of literals with exactly one positiveDisjunction of literals with exactly one positive–Equivalent to implication with conjunction of positive Equivalent to implication with conjunction of positive literals on left (antecedent / body / premise) and one literals on left (antecedent / body / premise) and one positive literal on right (consequent / head / conclusion)positive literal on right (consequent / head / conclusion)–Propositional logic used Horn clauses, which permit zero Propositional logic used Horn clauses, which permit zero oror one to be positive one to be positive•Look for rules with premises that are satisfied (use Look for rules with premises that are satisfied (use substitution to make matches) and add conclusions to KBsubstitution to make matches) and add conclusions to KBSearch and forward chaining•Which rules have premises that are Which rules have premises that are satisfied (modus ponens)?satisfied (modus ponens)?–A ^ E => C… nopeA ^ E => C… nope–B ^ D => E… yesB ^ D => E… yes–E ^ C ^ G ^ H => I… nopeE ^ C ^ G ^ H => I… nopeA ^ E = C… yesA ^ E = C… yesE ^ C ^ G ^ H ^ I… nopeE ^ C ^ G ^ H ^ I… nope one more try… yes one more try… yes•Which rules have premises that are Which rules have premises that are satisfied (modus ponens)?satisfied (modus ponens)?–A ^ E => C… nopeA ^ E => C… nope–B ^ D => E… yesB ^ D => E… yes–E ^ C ^ G ^ H => I… nopeE ^ C ^ G ^ H => I… nopeA ^ E = C… yesA ^ E = C… yesE ^ C ^ G ^ H ^ I… nopeE ^ C ^ G ^ H ^ I… nope one more try… yes one more try… yesBreadth FirstBreadth First•A, B, D, G, HA, B, D, G, H•A ^ E => CA ^ E => C•B ^ D => EB ^ D => E•E ^ C ^ G ^ H => IE ^ C ^ G ^ H => IBreadth FirstBreadth First•A, B, D, G, HA, B, D, G, H•A ^ E => CA ^ E => C•B ^ D => EB ^ D => E•E ^ C ^ G ^ H => IE ^ C ^ G ^ H => ISearch and forward chainingWould other search methods work?Would other search methods work?•Yes, this technique falls in standard domain of all searchesYes, this technique falls in standard domain of all searchesWould other search methods work?Would other search methods work?•Yes, this technique falls in standard domain of all searchesYes, this technique falls in standard domain of all searchesSearch and backward chainingStart with KB full of implicationsStart with KB full of implications•Find all implications with conclusion matching the queryFind all implications with conclusion matching the query•Add to fringe list the unknown premisesAdd to fringe list the unknown premises–Adding could be to front or rear of fringe (depth or breadth)Adding could be to front or rear of fringe (depth or breadth)Start with KB full of implicationsStart with KB full of implications•Find all implications with conclusion matching the queryFind all implications with conclusion matching the query•Add to fringe list the unknown premisesAdd to fringe list the unknown premises–Adding could be to front or rear of fringe (depth or breadth)Adding could be to front or rear of fringe (depth or breadth)Search and backward chaining•Are all the premises of I satisfied? NoAre all the premises of I satisfied? No–For each (C E G H) are each of their For each (C E G H) are each of their premises satisfied?premises satisfied?C? no, put its premises on fringeC? no, put its premises on fringe–For each (A and E) are their For each (A and E) are their premises satisfied?premises satisfied?A… yesA… yesE… no, add premisesE… no, add premisesfor each B and Dfor each B and DB… yesB… yesD… yesD… yes–E, G, H… yesE, G, H… yes•Are all the premises of I satisfied? NoAre all the premises of I satisfied? No–For each (C E G H) are each of their For each (C E G H) are each of their premises satisfied?premises