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, 718Examplex.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 {xa}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