DOC PREVIEW
Stanford CS 157 - Relational Proofs

This preview shows page 1-2-3-4-5-6 out of 19 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 19 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 19 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 19 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 19 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 19 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 19 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 19 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

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

Stanford CS 157 - Relational Proofs

Documents in this Course
Lecture 1

Lecture 1

15 pages

Equality

Equality

32 pages

Lecture 19

Lecture 19

100 pages

Epilog

Epilog

29 pages

Equality

Equality

34 pages

Load more
Download Relational Proofs
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Relational Proofs and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Relational Proofs 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?