Guest Speaker CS 416 Artificial Intelligence Topics in Optimal Control Minimax Control and Game Theory March 28th 2 p m OLS 005 Onesimo Hernandez Lerma Department of Mathematics CINVESTAV IPN Mexico City Lecture 15 First Order Logic Chapter 9 This is a nontechnical introduction mainly thru examples to some recent topics in control and game theory including adaptive control minimax control a k a worst case control or games against nature partially observable systems a k a controlled hidden Markov models cooperative and noncooperative game equilibria etc Final Exam Forward Chaining Final Exam will be May 6th at 7 00 p m Remember this from propositional logic Start with atomic sentences in KB Apply Modus Ponens This conflicts with the fewest number of other exams add new sentences to KB discontinue when no new sentences Hopefully find the sentence you are looking for in the generated sentences Lifting forward chaining Example The law says it is a crime for an American to sell weapons to hostile nations The country Nono an enemy of America has some missiles and all of its missiles were sold to it by Colonel West who is American First order definite clauses all sentences are defined this way to simplify processing disjunction of literals with exactly one positive clause is either atomic or an implication whose antecedent is a conjunction of positive literals and whose consequent is a single positive literal We will prove West is a criminal Page 1 Example Example We also need to know that missiles are weapons It is a crime for an American to sell weapons to hostile nations and we must know that an enemy of America counts as hostile Nono has some missiles Owns Nono M1 Missile M1 West who is American All of its missiles were sold to it by Colonel West The country Nono an enemy of America Forward chaining First iteration of forward chaining Starting from the facts Look at the implication sentences first find all rules with satisfied premises add their conclusions to known facts repeat until must satisfy unknown premises We can satisfy this rule query is answered no new facts are added by substituting x M1 and adding Sells West M1 Nono to KB First iteration of forward chaining Second iteration of forward chaining We can satisfy We can satisfy with x M1 and Weapon M1 is added with x West y M1 z Nono and Criminal West is added We can satisfy with x Nono and Hostile Nono is added Page 2 Analyze this algorithm Proving completeness Assume KB only has sentences with no function symbols Sound Does it only derive sentences that are entailed Yes because only Modus Ponens is used and it is sound What s the most number of iterations through algorithm Depends on the number of facts that can be added Let k be the arity the max number of arguments of any predicate and Let p be the number of predicates Let n be the number of constant symbols Complete Does it answer every query whose answers are entailed by the KB Yes if the clauses are definite clauses At most pnk distinct ground facts Fixed point is reached after this many iterations A proof by contradiction shows that the final KB is complete Complexit of this algorithm Pattern matching Three sources of complexity Conjunct ordering inner loop requires finding all unifiers such that premise of rule unifies with facts of database Missile x Owns Nono x Sells West x Nono Look at all items owned by Nono call them X for each element x in X check if it is a missile this pattern matching is expensive must check every rule on every iteration to check if its premises are satisfied many facts are generated that are irrelevant to goal Look for all missiles call them X for each element x in X check if it is owned by Nono Optimal ordering is NP hard similar to matrix mult Incremental forward chaining Irrelevant facts Pointless redundant repetition Some facts are irrelevant and occupy computation of forward chaining algorithm Some rules generate new information this information may permit unification of existing rules What if Nono example included lots of facts about food preferences some rules generate preexisting information we need not revisit the unification of the existing rules Not related to conclusions drawn about sale of weapons How can we eliminate them Every new fact inferred on iteration t must be derived from at least one new fact inferred on iteration t 1 Backward chaining is one way Page 3 Magic Set Backward Chaining Rewriting the rule set Start with the premises of the goal Sounds dangerous Add elements to premises that restrict candidates that will match Each premise must be supported by KB Start with first premise and look for support from KB looking for clauses with a head that matches premise the head s premise must then be supported by KB added elements are based on desired goal Let goal Criminal West A recursive depth first algorithm Magic x American x Weapon y Sells x y z Hostile z Criminal x Add Magic West to Knowledge Base Suffers from repetition and incompleteness Resolution First order CNF For all x American x Weapon y Sells x y z Hostile z Criminal x We saw earlier that resolution is a complete algorithm for refuting statements Must put first order sentences into conjunctive normal form American x V Weapon y V Sells x y z V Hostile z V Criminal x conjunction of clauses each is a disjunction of literals literals can contain variables which are assumed to be universally quantified Every sentence of first order logic can be converted into an inferentially equivalent CNF sentence they are both unsatisfiable in same conditions Example Example Everyone who loves all animals is loved by someone Page 4 Example Example F and G are Skolem Functions arguments of function are universally quantified variables in whose scope the existential quantifier appears Two clauses F x refers to the animal potentially unloved by x G x refers to someone who might love x Resolution inference rule Resolution A lifted version of propositional resolution rule two clauses must be standardized apart no variables are shared can be resolved if their literals are complementary one is the negation of the other if one unifies with the negation of the other Page 5