CS 561, Session 16-181Inference in First-Order Logic• Proofs• Unification• Generalized modus ponens• Forward and backward chaining• Completeness•Resolution• Logic programmingCS 561, 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 561, Session 16-183Logic as a representation of the WorldFactsWorldFactfollowsRefers to (Semantics)Representation: SentencesSentenceentailsCS 561, Session 16-184Desirable Properties of Inference ProceduresentailFollows – from-1derivationFactsFactSentences SentenceCS 561, Session 16-185Remember:propositionallogicCS 561, 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 561, Session 16-187ProofsCS 561, 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 561, 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 561, Session 16-1810Example ProofCS 561, Session 16-1811Example ProofCS 561, Session 16-1812Example ProofCS 561, Session 16-1813Example Proof4 & 5CS 561, Session 16-1814Search with primitive example rulesCS 561, Session 16-1815UnificationGoal of unification: finding σCS 561, Session 16-1816UnificationCS 561, Session 16-1817Extra example for unification{x/coke, x/Bob}Is it correct?Sells(x, coke)Sells(Bob, x){x/Bob}Student(Bob)Student(x)σQPCS 561, Session 16-1818Extra example for unification{x/coke, y/Bob}Sells(y, coke)Sells(Bob, x){x/Bob}Student(Bob)Student(x)σQPCS 561, 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 561, Session 16-1820Generalized Modus Ponens (GMP)CS 561, Session 16-1821Soundness of GMPCS 561, 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 561, 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 561, Session 16-1824Forward chainingCS 561, Session 16-1825Forward chaining exampleCS 561, Session 16-1826Example: Forward ChainingCurrent available rules• A ^ C => E• D ^ C => F• B ^ E => F• B => C• F => GCS 561, 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 561, Session 16-1828Backward chainingCS 561, Session 16-1829Backward chaining exampleCS 561, Session 16-1830A simple example• B^C=> G• A^G=> I• D^G=>J• E=> C• D^C=>K• F=>C•Q: I?CS 561, Session 16-1831A simple example• B^C=> G• A^G=> I• D^G=>J• E=> C• D^C=>K• F=>C•Q: I?1.A^G2. A?1.USER3. G?1.B^C1.USER2. E v FCS 561, Session 16-1832Another Example (from Konelsky)• Nintendo example.• Nintendo says it is Criminal for a programmer to provide emulators to people. My friends don’t have a Nintendo 64, but they use software that runs N64 games on their PC, which is written by Reality Man, who is a programmer.CS 561, Session 16-1833Forward Chaining• The knowledge base initially contains:• Programmer(x) ∧ Emulator(y) ∧ People(z) ∧Provide(x,z,y) Þ Criminal(x)• Use(friends, x) ∧ Runs(x, N64 games) ÞProvide(Reality Man, friends, x)•Software(x) ∧ Runs(x, N64 games) Þ Emulator(x)CS 561, Session 16-1834Forward ChainingProgrammer(x) ∧ Emulator(y) ∧ People(z) ∧ Provide(x,z,y) ÞCriminal(x) (1)Use(friends, x) ∧ Runs(x, N64 games) Þ Provide(Reality Man, friends, x) (2)Software(x) ∧ Runs(x, N64 games) Þ Emulator(x) (3)• Now we add atomic sentences to the KB sequentially, and call on the forward-chaining procedure:• FORWARD-CHAIN(KB, Programmer(Reality Man))CS 561, Session 16-1835Forward ChainingProgrammer(x) ∧ Emulator(y) ∧ People(z) ∧ Provide(x,z,y) Þ Criminal(x) (1)Use(friends, x) ∧ Runs(x, N64 games) Þ Provide(Reality Man, friends, x) (2)Software(x) ∧ Runs(x, N64 games) Þ Emulator(x) (3)Programmer(Reality Man) (4)• This new premise unifies with (1) withsubst({x/Reality Man}, Programmer(x))but not all the premises of (1) are yet known, so nothing further
View Full Document
Unlocking...