Relational ProofsLogical EntailmentPropositional InterpretationsRelational InterpretationsLogical Entailment and ProvabilityFormal ProofsOld Rules of InferenceUniversal GeneralizationExistential GeneralizationIdea for Universal InstantiationExamplesBoundingSubstitutabilityUniversal InstantiationExistential Instantiation ISlide 16Existential Instantiation IISlide 18Slide 19ExampleHarry and RalphHarry and Ralph (continued)Slide 23Mendelson LogicMendelson Rules of InferenceMendelson Axiom SchemataProvabilitySoundness and CompletenessPropositional MetatheoremsResultsDeduction TheoremRelational Deduction TheoremRelational ProofsComputational Logic Lecture 7Michael Genesereth Autumn 20092Logical EntailmentA set of premises logically entails a conclusion ( |= ) if and only if every interpretation that satisfies also satisfies .3Propositional Interpretationsp q r0 0 00 0 10 1 00 0 11 0 01 0 11 1 01 1 1For a language with n constants, there are 2n interpretations.4Relational Interpretations |i| a b r{,} {}{,} {}{,} {}{,} {, }{,} {}{,} {}{,} {}{,} {, }{,} {}{,} {}{,} {}{,} {, } . . .Infinitely many interpretations!5Logical Entailment and ProvabilityGood News: If logically entails , then there is a finite proof of from . And vice versa.More Good News: If logically entails , it is possible to find such a proof in finite time.Sad News: If does not logically entail , the process of finding a proof may run forever.Not So Bad News: In many cases, the process can be stopped after finitely many steps.6Formal ProofsA formal proof of from is a sequence of sentences terminating in in which each item is either:1. a premise (a member of )2. an instance of an axiom schema3. the result of applying a rule of inference to earlier items in the sequence.7Old Rules of InferenceModus Ponens (MP) Modus Tolens (MT)And Introduction (AI) And Elimination (AE)ϕ ⇒ ψϕψϕ ⇒ ψ¬ψ¬ϕϕ ∧ψϕψϕψϕ ∧ψ8Universal GeneralizationRule of InferenceExamples: p(x) p(x) q(x) x.p(x) x.(p(x) q(x))€ ϕ∀ν.ϕ9Existential GeneralizationRule of InferenceExamples: p(a) p(a) q(a) x.p(x) x.(p(x) q(x))€ ϕ[τ]∃ν.ϕ [ν]10Idea for Universal Instantiation€ ∀ν.ϕϕ [ν ← τ]Warning: This is not quite right.11Examplesy.hates(jane,y)hates(jane,jill) yjillhates(jane,mother(jane)) ymother(jane)hates(jane,y) yyhates(jane,z) yzx.y.hates(x,y)y.hates(jane,y) xjaney.hates(y,y) xy Wrong!!12BoundingA term is bound by in if and only if contains a variable and there is some free occurrence of in and that occurrence lies in the scope of a quantifier of .mother(x) is bound by y in x.hates(x ,y).Why? The term mother(x) contains a variable x. There is a free occurrence of y in x.hates(x,y). That occurrence of y lies in scope of quantifier of x.13SubstitutabilityA term is substitutable for in if and only if it is not bound by in .Some texts say “x is free for y in ” instead of “x is substitutable for y in ”.mother(jane) is free for y in hates(jane,y).mother(x) is free for y in hates(jane,y).mother(x) is free for y in z.hates(z,y).mother(x) is not free for y in x.hates(x,y).mother(x) is free for y in (x.y.l(x,y) z.h(z,y)).14Universal Instantiation€ ∀ν.ϕϕ [ν ← τ]where τ is free for ν in ϕ15Existential Instantiation I€ ∃ν.ϕϕ [ν ← σ ]where ∃ν.ϕ contains no free variableswhere σ is a new object constant16Examplesy.p(y)p(c)y.y*y=01*1=0 Wrong!y.y*y=xc*c=x Wrong!c*c=4c*c=617Existential Instantiation II€ ∃ν.ϕϕ [ν ← π(τ1,...,τn)]where τ1,...,τn are free in ∃ν.ϕwhere π is a new function constant18Examplesy.y*y=xf(x)*f(x)=xf(4)*f(4)=4f(6)*f(6)=6y.y*y=xsqrt(x)*sqrt(x)=xlog(x)*log(x)=x Wrong!19Formal ProofsA formal proof of from is a sequence of sentences terminating in in which each item is either:1. a premise (a member of )2. an instance of an axiom schema3. the result of applying a rule of inference to earlier items in the sequence.20ExampleEverybody loves somebody. Everybody loves a lover. Show that Jack loves Jill.1. ∀x.∃y.loves(x,y) Premise2. ∀u.∀v.∀w.(loves(v,w) ⇒ loves(u,v)) Premise3. ∃y.loves(jill,y) UI :14. loves(jill,mike) EI :35. ∀v.∀w.(loves(v,w) ⇒ loves(jack,v)) UI : 26. ∀w.(loves(jill,w)⇒ loves(jack, jill)) UI : 57. loves(jill,mike)⇒ loves(jack, jill) UI : 68. loves(jack, jill) MP :7,421Harry and RalphEvery horse can outrun every dog. Some greyhounds can outrun every rabbit. Harry is a horse. Ralph is a rabbit. Can Harry outrun Ralph?1. ∀x.∀y.(h(x)∧d(y)⇒ f(x,y)) Premise2. ∃y.(g(y)∧∀z.(r(z)⇒ f(y,z))) Premise3. ∀y.(g(y) ⇒ d(y)) Premise4. ∀x.∀y.∀z.(f(x,y)∧ f(y,z) ⇒ f(x,z)) Premise5. h(harry) Premise6. r(ralph) Premise22Harry and Ralph (continued)€ 7. g(greg)∧∀z.(r(z) ⇒ f (greg, z)) EI : 28. g(greg) AE : 79. ∀z.(r(z) ⇒ f (greg, z)) AE : 710. r(ralph) ⇒ f (greg,ralph) UI : 911. f (greg,ralph) MP :6,1012. g(greg) ⇒ d(greg) UI : 313. d(greg) MP :12,814. ∀y.(h(harry)∧d(y) ⇒ f (harry, y)) UI :115. h(harry)∧d(greg) ⇒ f (harry, greg) UI :1416. h(harry)∧d(greg) AI : 5,1317. f (harry, greg) MP :15,1623Harry and Ralph (continued)18. ∀y.∀z.(f(harry,y)∧ f(y,z) ⇒ f(harry,z)) UI : 419. ∀z.(f(harry,greg)∧ f(greg,z) ⇒ f(harry,z)) UI :1820. f(harry,greg)∧ f(greg,ralph)⇒ f(harry,ralph)) UI :1921. f(harry,greg)∧ f(greg,ralph) AI :17,1122. f(harry,ralph) MP :20,2124Mendelson LogicMendelson Logic is that subset of Relational Logic in which there are only two operators, viz. and , and one quantifier, viz. . Fortunately, all sentences in Relational Logic can be reduced to logically equivalent sentences with these operators by applying the following rules.( ) (( ) ( ))( ) ( ) ( ) ( ) ( ) ( ) . .25Mendelson Rules of InferenceModus Ponens (MP)Universal Generalization (UG)€
View Full Document
Unlocking...