DOC PREVIEW
Stanford CS 157 - Resolution Theorem Proving

This preview shows page 1-2-15-16-31-32 out of 32 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 32 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 32 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 32 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 32 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 32 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 32 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 32 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

Resolution Theorem ProvingPlanPropositional ResolutionRelational Resolution IExampleSlide 6Slide 7Example (continued)Example (concluded)Harry and RalphHarry and Ralph (continued)Slide 12Harry and Ralph (concluded)Slide 14Slide 15Slide 16Slide 17Slide 18Slide 19Slide 20ProblemRelational Resolution IISlide 23Problem Without Repeated RenamingSolution With Repeated RenamingSlide 26FactorsRelational Resolution III (Final Version)Slide 29Need for Original ClausesProvabilitySoundness and CompletenessResolution Theorem ProvingComputational Logic Lecture 11Michael Genesereth Autumn 20102PlanFirst Lecture - Resolution PreliminariesUnificationRelational Clausal FormSecond Lecture - Resolution PrincipleResolution Principle and FactoringResolution Theorem ProvingThird Lecture - Resolution Applications Theorem ProvingAnswer ExtractionReductionFourth Lecture - Resolution StrategiesElimination Strategies (tautology elimination, subsumption, …)Restriction Strategies (ancestry filtering, set of support, …)3Propositional Resolution€ {ϕ1,...,ϕ ,...,ϕm}{ψ1,...,¬ ϕ ,...,ψn}{ϕ1,...,ϕm,ψ1,...,ψn}4Relational Resolution I€ {ϕ1,..., ϕ ,...,ϕm}{ψ1,...,¬ ψ,...,ψn}{ϕ1,...,ϕm,ψ1,...,ψn}σwhere σ = mgu(ϕ ,ψ )5Example€ { p(a, y),r(y)}{¬ p(x,b)}{r(y)}{x ← a, y ← b}{r(b)}6Example€ { p(a, y), r(y)}{¬ p(x, f (x)),q(g(x))}{r(y),q(g(x))}{x ← a, y ← f (a)}{r( f (a)),q(g(a))}7ExampleEverybody loves somebody. Everybody loves a lover. Show that everybody loves everybody.€ ∀x.∃y.loves(x, y)∀u.∀v.∀w.(loves(v,w) ⇒ loves(u,v))¬∀ x.∀ y.loves(x, y)8Example (continued)€ ∀x.∃y.loves(x, y)∀u.∀ v.∀w.(loves(v,w) ⇒ loves(u,v))¬∀ x.∀ y.loves(x, y){loves(x, f (x))}{¬ loves(v,w),loves(u,v)}{¬ loves( jack, jill)}9Example (concluded)€ 1. {loves(x, f (x))} Premise2. {¬ loves(v,w),loves(u,v)} Premise3. {¬ loves( jack, jill)} Goal4. {loves(u, x)} 1,25. {} 4,310Harry and RalphEvery horse can outrun every dog. Some greyhound can outrun every rabbit. Show that every horse can outrun every rabbit.€ ∀x.∀y.(h(x)∧d(y) ⇒ f (x, y))∃y.(g(y)∧∀z.(r(z) ⇒ f (y, z)))∀y.(g(y) ⇒ d(y))∀x.∀y.∀z.( f (x, y)∧ f (y,z) ⇒ f (x,z))¬∀ x.∀ y.(h(x)∧r(y) ⇒ f (x, y))11Harry and Ralph (continued)€ ∀x.∀y.(h(x)∧d(y) ⇒ f (x, y))∃y.(g(y)∧∀z.(r(z) ⇒ f (y, z)))∀y.(g(y) ⇒ d(y))∀x.∀y.∀z.( f (x, y)∧ f (y,z) ⇒ f (x,z)){¬ h(x),¬ d(y), f (x, y)}{g(greg)}{¬ r(z), f (greg,z)}{¬ g(y),d(y)}{¬ f (x, y),¬ f (y, z), f (x,z)}12Harry and Ralph (continued)€ ¬∀x.∀ y.(h(x)∧r(y) ⇒ f (x, y)){h(harry)}{r(ralph)}{¬ f (harry,ralph)}13Harry and Ralph (concluded)€ 1. {¬ h(x),¬ d(y), f (x, y)}2. {g(greg)}3. {¬ r(z), f (greg,z)}4. {¬ g(y),d(y)}5. {¬ f (x, y),¬ f (y,z), f (x,z)}6. {h(harry)}7. {r(ralph)}8. {¬ f (harry,ralph)}€ 9. {d(greg)}10. {¬ d(y), f (harry, y)}11. { f (harry,greg)}12. { f (greg,ralph)}13. {¬ f (greg,z), f (harry, z)}14. { f (harry,ralph)}15. {}14ExampleGiven:x.y.(p(x,y)  q(x,y))x.y.(p(x,y)  q(x,y))Prove:x.y.(p(x,y)  q(x,y))15Example (continued)x.y.(p(x,y)  q(x,y)) x.y.((p(x,y)  q(x,y))  (p(x,y)  q(x,y))) (p(a,y)  q(a,y))  (p(a,y)  q(a,y)) {p(a,y), q(a,y)} {p(a,y), q(a,y)}x.y.(p(x,y)  q(x,y)) p(x, f(x))  q(x, f(x)) {p(a,f(x)), q(a,f(x))}16Example (continued)Negate the goal: x.y.(p(x,y)  q(x,y))  x.y.(p(x,y)  q(x,y))Convert to Clausal Form: x.y.(p(x,y)  q(x,y)) x.y.(p(x,y)  q(x,y)) x.y.(p(x,y)  q(x,y)) p(x,y)  q(x,y) {p(x,y), q(x,y)}17Example (concluded)1. {p(a,y), q(a,y)} Premise2. {p(a,y), q(a,y)} Premise3. {p(x, f(x)), q(x, f(x))} Premise4. {p(x,y), q(x,y)} Negated Goal5. {q(a, f(a))} 1, 36. {p(a, f(a))} 2, 37. {p(a, f(a))} 4, 58. {} 6, 718Examplex.p(x)  y.p(y)19Example (continued)(x.p(x)  y.p(y)) I: (x.p(x)  y.p(y)) N: x.p(x)  y.p(y)x.p(x)  y.p(y) S: x.p(x)  y.p(y) E: x.p(x)  p(a) A: p(x)  p(a) D: p(x)  p(a) O: {p(x)} and {p(a)}20Example (concluded)Resolution:1. {p(x)} Premise2. {p(a)} Premise3. {} 1,2 {xa}21Problem€ { p(a, x)}{¬ p(x,b)}Failure22Relational Resolution II€ {ϕ1,..., ϕ ,...,ϕm}{ψ1,...,¬ ψ,...,ψn}{ϕ1τ,...,ϕmτ,ψ1,...,ψn}σwhere σ = mgu(ϕτ,ψ )where τ is a variable renaming on ϕ23Example€ { p(a, x)}{¬ p(x,b)}Failure€ { p(a, y)}{¬ p(x,b)}{}{x ← a, y ← b}24Problem Without Repeated Renaming1. {r(a,b,u1)} Premise2. {r(b,c,u2)} Premise3. {r(c,d,u3)} Premise4. {r(x,z,f(v)),r(x,y,f(f(v))),r(y,z,f(f(v)))} Premise5. {r(a,d,w)} Goal6. {r(a,y,f(f(v))),r(y,d,f(f(v)))} 4,57. {r(b,d,f(f(v)))} 1,68. Failure 4,725Solution With Repeated Renaming1. {r(a,b,u1)} Premise2. {r(b,c,u2)} Premise3. {r(c,d,u3)} Premise4. {r(x,z,f(v)),r(x,y,f(f(v))),r(y,z,f(f(v)))} Premise5. {r(a,d,w)} Goal6. {r(a,y6,f(f(v6))),r(y6,d,f(f(v6)))} 4,57. {r(b,d,f(f(v7)))} 1,68. {r(b,y8,f(f(f(v8)))),r(y8,d,f(f(f(v8))))} 4,79. {r(c,d,f(f(f(v9))))} 2,810. {} 3,926Problem€ {p(x), p(y)}{¬ p(u),¬ p(v)}{p(y),¬ p(v)}{p(x),¬ p(v)}{p(y),¬ p(u)}{p(x),¬ p(u)}27FactorsIf a subset of the literals in a clause  has a most general unifier , then the clause ' obtained by applying  to  is called a factor of .Clause{p(x),p(f(y)),r(x,y)}Factors{p(f(y)),r(f(y),y)}{p(x),p(f(y)),r(x,y)}28Relational Resolution III (Final Version)€ ΦΨ((Φ'−{φ})τ ∪(Ψ '−{¬ ψ}))σwhere φ∈ Φ', a factor of Φ where ¬ ψ ∈ Ψ ', a factor of Ψ where σ = mgu(ϕτ,ψ )where τ is a variable renaming on ϕ29Example€ {p(x), p(y)}{¬ p(u),¬ p(v)}{p(y),¬ p(v)}{p(x),¬ p(v)}{p(y),¬ p(u)}{p(x),¬ p(u)}€ {p(x)}{¬ p(u)}{}30Need for Original Clauses1. {p(a,y), p(x,b)} Premise2. {p(a,d)} Premise3. {p(c,b)} Premise4. {p(x,b)} 1,25. {} 3,41. {p(a,y), p(x,b)} Premise2. {p(a,d)} Premise3. {p(c,b)} Premise4. {p(a,b)} Factor of 131ProvabilityA resolution derivation of a clause  from a set  of clauses is a sequence of clauses terminating in  in which each item is(1) a member of  or(2) the result of applying the resolution to earlier items.A sentence  is provable from a set of sentences  byresolution if and only if there is a derivation of the empty clause from the


View Full Document

Stanford CS 157 - Resolution Theorem Proving

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 Resolution Theorem Proving
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 Resolution Theorem Proving 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 Resolution Theorem Proving 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?