Inference in First-Order LogicSlide 2Logic as a representation of the WorldDesirable Properties of Inference ProceduresRemember: propositional logicReminderProofsSlide 8Slide 9Example ProofSlide 11Slide 12Slide 13Search with primitive example rulesUnificationSlide 16Extra example for unificationSlide 18More Unification ExamplesGeneralized Modus Ponens (GMP)Soundness of GMPProperties of GMPHorn formForward chainingForward chaining exampleExample: Forward ChainingSlide 27Slide 28Slide 29Slide 30Slide 31Inference exampleBackward chainingBackward chaining exampleA simple exampleSlide 36Another Example (from Konelsky)Forward ChainingSlide 39Slide 40Slide 41Slide 42Slide 43Slide 44Slide 45Slide 46Slide 47Slide 48Slide 49Slide 50Slide 51Slide 52Slide 53Backward ChainingSlide 55Slide 56Slide 57Slide 58Slide 59Slide 60Slide 61Slide 62Slide 63Slide 64Slide 65Slide 66Slide 67Slide 68Slide 69Slide 70Slide 71Slide 72Slide 73CompletenessSlide 75Slide 76Slide 77Completeness in FOLHistorical noteKinship ExampleRefutation Proof/GraphResolutionResolution inference ruleRemember: normal formsConjunctive normal formSkolemizationExamples: Converting FOL sentences to clause form…Slide 88Slide 89Resolution proofSlide 91Slide 92Reference in First-Order LogicSlide 94Example of Refutation Proof (in conjunctive normal form)Slide 96Slide 97Question:CS 460, Session 16-181Inference in First-Order Logic•Proofs•Unification•Generalized modus ponens•Forward and backward chaining•Completeness•Resolution•Logic programmingCS 460, Session 16-182Inference in First-Order Logic•Proofs – extend propositional logic inference to deal with quantifiers•Unification•Generalized modus ponens•Forward and backward chaining – inference rules and reasoningprogram•Completeness – Gödel’s theorem: for FOL, any sentence entailed byanother set of sentences can be proved from that set•Resolution – inference procedure that is complete for any set ofsentences•Logic programmingCS 460, Session 16-183Logic as a representation of the WorldFactsWorldFactfollowsRefers to (Semantics)Representation: SentencesSentenceentailsCS 460, Session 16-184Desirable Properties of Inference Proceduresentail Follows – from-1derivationFactsFactSentences SentenceCS 460, Session 16-185Remember:propositionallogicCS 460, Session 16-186Reminder•Ground term: A term that does not contain a variable.•A constant symbol•A function applies to some ground term•{x/a}: substitution/binding listCS 460, Session 16-187ProofsCS 460, Session 16-188ProofsThe three new inference rules for FOL (compared to propositional logic) are:•Universal Elimination (UE):for any sentence , variable x and ground term ,x  {x/}•Existential Elimination (EE):for any sentence , variable x and constant symbol k not in KB,x {x/k}•Existential Introduction (EI):for any sentence , variable x not in  and ground term g in , x {g/x}CS 460, Session 16-189ProofsThe three new inference rules for FOL (compared to propositional logic) are:•Universal Elimination (UE):for any sentence , variable x and ground term ,x  e.g., from x Likes(x, Candy) and {x/Joe} {x/} we can infer Likes(Joe, Candy)•Existential Elimination (EE):for any sentence , variable x and constant symbol k not in KB,x  e.g., from x Kill(x, Victim) we can infer{x/k} Kill(Murderer, Victim), if Murderer new symbol•Existential Introduction (EI):for any sentence , variable x not in  and ground term g in ,  e.g., from Likes(Joe, Candy) we can inferx {g/x} x Likes(x, Candy)CS 460, Session 16-1810Example ProofCS 460, Session 16-1811Example ProofCS 460, Session 16-1812Example ProofCS 460, Session 16-1813Example ProofCS 460, Session 16-1814Search with primitive example rulesCS 460, Session 16-1815UnificationGoal of unification: finding σCS 460, Session 16-1816UnificationCS 460, Session 16-1817Extra example for unificationP Q σStudent(x) Student(Bob) {x/Bob}Sells(Bob, x) Sells(x, coke) {x/coke, x/Bob}Is it correct?CS 460, Session 16-1818Extra example for unificationP Q σStudent(x) Student(Bob) {x/Bob}Sells(Bob, x) Sells(y, coke) {x/coke, y/Bob}CS 460, Session 16-1819More Unification Examples1 – unify(P(a,X), P(a,b)) σ = {X/b}2 – unify(P(a,X), P(Y,b)) σ = {Y/a, X/b}3 – unify(P(a,X), P(Y,f(a)) σ = {Y/a, X/f(a)}4 – unify(P(a,X), P(X,b)) σ = failureNote: If P(a,X) and P(X,b) are independent, then we can replace X with Y and get the unification to work.VARIABLE termCS 460, Session 16-1820Generalized Modus Ponens (GMP)CS 460, Session 16-1821Soundness of GMPCS 460, Session 16-1822Properties of GMP•Why is GMP and efficient inference rule?- It takes bigger steps, combining several small inferences into one- It takes sensible steps: uses eliminations that are guaranteedto help (rather than random UEs)- It uses a precompilation step which converts the KB to canonicalform (Horn sentences)Remember: sentence in Horn from is a conjunction of Horn clauses(clauses with at most one positive literal), e.g.,(A  B)  (B  C   D), that is (B  A)  ((C  D)  B)CS 460, Session 16-1823Horn form•We convert sentences to Horn form as they are entered into the KB•Using Existential Elimination and And Elimination•e.g., x Owns(Nono, x)  Missile(x) becomesOwns(Nono, M)Missile(M)(with M a new symbol that was not already in the KB)CS 460, Session 16-1824Forward chainingCS 460, Session 16-1825Forward chaining exampleCS 460, Session 16-1826Example: Forward ChainingCurrent available rules•A ^ C => E•D ^ C => F•B ^ E => F•B => C•F => GCS 460, Session 16-1827Example: Forward ChainingCurrent available rules•A ^ C => E (1)•D ^ C => F (2)•B ^ E => F (3)•B => C (4)•F => G (5)Percept 1. A (is true)Percept 2. B (is true)then, from (4), C is true, then the premises of (1) will be satisfied, resulting to make E true, then the premises of (3) are going to be satisfied, thus F is true, and finally from (5) G is true.CS 460, Session 16-1828Example of Deduction: What can we prove? s(Y,Z) /\ r(Z) → r(Y) r(a).s(b,c)s(c,a).¬r(c)CS 460, Session 16-1829¬s(Y,Z) \/ ¬r(Z) \/ r(Y) r(a).s(b,c)s(c,a).¬r(c) ¬s(Y,Z) \/ ¬r(Z) \/ r(Y) s(c,a)  = {Y/c, Z/a} ¬r(a) \/ r(c) r(a) r(c) ¬r(c) [ ]Example of Deduction: What can we prove?CS 460, Session 16-1830¬s(Y,Z) \/ ¬r(Z) \/ r(Y)