Relational ProofsLogical EntailmentPropositional InterpretationsRelational InterpretationsLogical Entailment and ProvabilityFormal ProofsOld Rules of InferenceUniversal GeneralizationExistential GeneralizationIdea for Universal InstantiationExamplesBoundingSubstitutabilityInappropriatenessSlide 15Universal InstantiationExistential Instantiation ISlide 18Existential Instantiation IISlide 20Slide 21ExampleHarry and RalphHarry and Ralph (continued)Slide 25Mendelson LogicMendelson Rules of InferenceMendelson Axiom SchemataProvabilityDecidabilitySemidecidabilitySemidecidability of Logical EntailmentDecidability Not ProvedUndecidability of Logical EntailmentUndecidability (continued)ClosureTheoriesRelationships on TheoriesArithmetization of Logical EntailmentIncompleteness TheoremSummaryRelational ProofsComputational Logic Lecture 7Michael Genesereth Autumn 20072Logical EntailmentA set of premises logically entails a conclusion if and only if every interpretation that satisfies the premises also satisfies the conclusion.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)).14InappropriatenessAn occurrence of a term is inappropriate for a variable in if and only if contains a variable and there is some free occurrence of in that lies in the scope of a quantifier of .mother(x) is inappropriate for y in x.hates(x,y).15SubstitutabilityA term is substitutable for in if and only if it is not inappropriate with 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)).16Universal Instantiation€ ∀ν.ϕϕ [ν ← τ]where τ is free for ν in ϕ17Existential Instantiation I€ ∃ν.ϕϕ [ν ← σ ]where ∃ν.ϕ contains no free variableswhere σ is a new object constant18Examplesy.p(y)p(c)y.y*y=01*1=0 Wrong!y.y*y=xc*c=x Wrong!c*c=4c*c=619Existential Instantiation II€ ∃ν.ϕϕ [ν ← π(τ1,...,τn)]where τ1,...,τn are free in ∃ν.ϕwhere π is a new function constant20Examplesy.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!21Formal 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.22ExampleEverybody 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,423Harry 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) Premise24Harry 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
View Full Document
Unlocking...