1Relational ProofsComputational Logic Lecture 8Michael Genesereth Spring 20052Logical EntailmentA set of premises logically entails a conclusion if andonly if every interpretation that satisfies the premisesalso satisfies the conclusion.23Herbrand SummaryHerbrand Method works for Basic and UniversalLogic, but there can be many interpretations.Herbrand Method does not work for Existential Logicunless sentences rewritten in Functional Logic.Herbrand Method works for Functional Logic, butinfinitely many interpretationsSolution: Use formal proofs!4Formal ProofsA formal proof of ϕ from Δ is a sequence ofsentences terminating in ϕ in which each item iseither:1. a premise (a member of Δ)2. an instance of an axiom schema3. the result of applying a rule of inference toearlier items in the sequence.35Old Rules of InferenceModus Ponens (MP) Modus Tolens (MT)And Introduction (AI) And Elimination (AE)ϕ⇒ψϕψϕ⇒ψ¬ψ¬ϕϕ∧ψϕψϕψϕ∧ψ6Universal GeneralizationRule of InferenceExamples: p(x) p(x) ⇒ q(x) ∀x.p(x) ∀x.(p(x) ⇒ q(x))€ ϕ∀ν.ϕ47Existential GeneralizationRule of InferenceExamples: p(a) p(a) ∨ q(a) ∃x.p(x) ∃x.(p(x) ∨ q(x))€ ϕ[τ]∃ν.ϕ[ν]8Idea for Universal Instantiation∀ν.ϕϕ[ν←τ]Warning: This is not quite right.59Examples∀y.hates(jane,y)hates(jane,jill) y←jillhates(jane,mother(jane)) y←mother(jane)hates(jane,y) y←yhates(jane,z) y←z∀x.∃y.hates(x,y)∃y.hates(jane,y) x←jane∃y.hates(y,y) x←y Wrong!!10BoundingA term τ is bound by ν in ϕ if and only if τ contains avariable µ 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.611SubstitutabilityA term τ is substitutable for ν in ϕ if and only if it isnot bound by ν in ϕ.Some texts say “x is free for y in ϕ” instead of “x issubstitutable 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)).12InappropriatenessAn occurrence of a term τ is inappropriate for avariable ν in ϕ if and only if τ contains a variable µand there is some free occurrence of ν in ϕ that liesin the scope of a quantifier of µ.mother(x) is inappropriate for y in ∃x.hates(x,y).713SubstitutabilityA term τ is substitutable for ν in ϕ if and only if it isnot inappropriate with ν in ϕ.Some texts say “x is free for y in ϕ” instead of “x issubstitutable 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 ϕ815Existential Instantiation I∃ν.ϕϕ[ν←σ]where ϕ contains no free variableswhere σ is a new object constant16Examples∃y.p(y)p(c)∃y.y*y=01*1=0 Wrong!∃y.y*y=xc*c=x Wrong!c*c=4c*c=6917Existential Instantiation II∃ν.ϕϕ[ν←π(τ1,...,τn)]where τ1,...,τn are free in ϕwhere π is a new function constant18Examples∃y.y*y=xf(x)*f(x)=xf(4)*f(4)=4f(6)*f(6)=6∃y.y*y=xsqrt(x)*sqrt(x)=xlog(x)*log(x)=x Wrong!1019Formal ProofsA formal proof of ϕ from Δ is a sequence ofsentences terminating in ϕ in which each item iseither:1. a premise (a member of Δ)2. an instance of an axiom schema3. the result of applying a rule of inference toearlier items in the sequence.20ExampleEverybody loves somebody. Everybody loves alover. 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, 41121Harry and RalphEvery horse can outrun every dog. Some greyhounds canoutrun every rabbit. Harry is a horse. Ralph is a rabbit. CanHarry 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 : 38. 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, 161223Harry 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, 2124Standard Axiom SchemataII: ϕ ⇒ (ψ ⇒ ϕ)ID: (ϕ ⇒ (ψ ⇒ χ)) ⇒ ((ϕ ⇒ ψ) ⇒ (ϕ ⇒ χ))CR: (¬ψ ⇒ ϕ) ⇒ ((¬ψ ⇒ ¬ϕ) ⇒ ψ)(ψ ⇒ ϕ ) ⇒ ((ψ ⇒ ¬ϕ) ⇒ ¬ψ)EQ: (ϕ ⇔ ψ) ⇒ (ϕ ⇒ ψ)(ϕ ⇔ ψ) ⇒ (ψ ⇒ ϕ)(ϕ ⇒ ψ) ⇒ ((ψ ⇒ ϕ) ⇒ (ϕ ⇔ ψ))OQ:!! (ϕ ⇐ ψ) ⇔ (ψ ⇒ ϕ)(ϕ ∨ ψ) ⇔ (¬ϕ ⇒ ψ)(ϕ ∧ ψ) ⇔ ¬(¬ϕ ∨ ¬ψ )1325Standard Axiom Schemata (concluded)UD: ∀ν.(ϕ ⇒ ψ) ⇒ (∀ν.ϕ ⇒∀ν.ψ)UG: ϕ ⇒ ∀ν.ϕwhere ν is not free in ϕUI: ∀ν.ϕ ⇒ ϕ[ν←τ]where τ is free for ν in !ϕED: ∃ν.ϕ ⇔¬∀ν.¬ϕ26ProvabilityA sentence ϕ is provable from a set of sentences Δ ifand only if there is a finite formal proof of ϕ from Δusing only Modus Ponens, Universal generalization,and the standard axiom schemata.Soundness Theorem: If ϕ is provable from Δ, then Δlogically entails ϕ.Completeness Theorem (Godel): If Δ logically entailsϕ, then ϕ is provable from Δ.1427DecidabilityA class of questions is decidable if and only if there isa procedure such that, when given as input anyquestion in the
View Full Document