1StrategiesComputational Logic Lecture 13Michael Genesereth Autumn 20102PlanFirst Lecture - Resolution PreliminariesUnificationRelational Clausal FormSecond Lecture - Resolution PrincipleResolution Principle and FactoringResolution Theorem ProvingThird Lecture - Resolution Applications Theorem ProvingAnswer ExtractionResidueFourth Lecture - Resolution StrategiesElimination Strategies (tautology elimination, subsumption, …)Restriction Strategies (ancestry filtering, set of support, …)23Proof1. {p, q} p ∨ q2. {p, ¬q} p ∨ ¬q3. {¬p, q} ¬p ∨ q4. {¬p, ¬q} ¬p ∨ ¬q5. {p} 1,26. {¬p} 3,47. {} 5,64PoemWe shall not cease from exploration,And the end of all our exploringWill be to arrive where we startedAnd know the place for the first time.T. S. Eliot35Proof as Produced by Two Finger Method1. {p,q} p ∨ q2. {p, ¬q} p ∨ ¬q3. {¬p, q} ¬p ∨ q4. {¬p, ¬q} ¬p ∨ ¬q5. {p} 1,26. {q} 1,37. {¬q, q} 2, 38. {p, ¬p} 2, 39. {q, ¬q} 1,49.5 {p, ¬p} 1,410. {¬q} 2, 411. {¬p} 3, 412. {q} 3,513. {¬q} 4, 514. {p} 2, 615. {¬p} 4, 616. {p,q} 1,717. {¬q, p} 2, 718. {¬p, q} 3, 719. {¬q, ¬p} 4, 720. {q} 6, 76Proof (continued)21. {¬q, q} 7, 722. {¬q, q} 7, 723. {q, p} 1,824. {¬q, p} 2, 825. {¬p, q} 3,826. {¬p, ¬q} 4, 827. {p} 5,828. {¬p, p} 8,829. {¬p, p} 8,830. {p, q} 1,931. {¬q, p} 2, 932. {¬p, q} 3,933. {¬q, ¬p} 4, 934. {q} 6, 935. {¬q, q} 7,936. {q, ¬q} 9, 937. {q, ¬q} 9, 938. {p} 1,1039. {¬p} 3,1040. {} 6,1047StrategiesElimination Strategies (Constraints on clauses):Identical Clause EliminationPure Literal EliminationTautology EliminationSubsumption EliminationRestriction Strategies (Constraints on inferences):Unit RestrictionInput RestrictionLinear RestrictionSet of Support Restriction8Identical Clause EliminationMetatheorem: There is a resolution refutation of Δ ifand only if there is a resolution refutation from Δ inwhich no clause occurs twice. (Obvious.)Upshot: If you generate a clause that is already in theproof, do not include it again.59Proof With Identical Clause Elimination1. {p,q} p ∨ q2. {p, ¬q} p ∨ ¬q3. {¬p, q} ¬p ∨ q4. {¬p, ¬q} ¬p ∨ ¬q5. {p} 1,26. {q} 1,37. {¬q, q} 2,38. {p, ¬p} 2, 39. {q, ¬q} 1,410. {¬q} 2, 411. {¬p} 3, 412. {} 6,1010Motivation for Tautology Elimination1. {p,q} Premise2. {p,¬p} Premise3. {p,q} 1,2611Tautology EliminationA tautology is a clause with a complementary pair ofliterals.{q,¬q}{p, q, r,¬q}{p(x), q(a,y),¬q(a,y), r(z)}Metatheorem: There is a resolution refutation of Δ ifand only if there is a resolution refutation from Δ withtautology elimination.12Proof with TE and ICE1. {p, q} p ∨ q2. {p, ¬q} p ∨ ¬q3. {¬p, q} ¬p ∨ q4. {¬p, ¬q} ¬p ∨ ¬q5. {p} 1,26. {q} 1,37. {¬q} 2, 48. {¬p} 3,49. {} 6, 7713NoteNon-Tautology:{p(x), ¬p(a)}Reason for Non-Example: {!p(x), ¬p(a)} {p(a)} {¬p(b)}14Motivation for Subsumption1. {p, q} Premise2. {p, q, r} Premise3. {q,r} Premise4. {¬p} Premise5. {¬q} Premise6. {¬r} Premise815Propositional SubsumptionA clause Φ subsumes Ψ if and only if Φ is a subset ofΨ.Example: {p, q} subsumes {p, q, r}Theorem: There is a resolution refutation of Δ if andonly if there is a resolution refutation from Δ withPropositional Subsumption.16NoteThe resolution of two clauses sometimes produces aclause that subsumes one of its parents.1. {p} Premise2. {¬r,q} Premise3. {r} Premise4. {¬p, ¬q,¬r} Premise5. {¬q,¬r} 1, 46. {¬r} 2, 57. {} 3,6917Relational SubsumptionA relational clause Φ subsumes Ψ if and only if thereis a substitution σ that, when applied to Φ, produces aclause Φσ that is a subset of Ψ.{¬!p(a,b), q(c)}{¬p(x,y)}Why:{¬p(x,y)}{x←a,y←b} = {¬p(a,b)} ⊆ {¬!p(a,b), q(c)}Metatheorem: There is a resolution refutation of Δ ifand only if there is a resolution refutation from Δ withsubsumption.18NoteNon-Example:{¬!p(x,b), q(x)}{¬p(a,y)}Reason for Non-Example:{¬!p(x,b), q(x)}{¬p(a,y)}{p(b,b)}{¬q(b)}1019Example for Pure Literal Elimination1. {p, q} Premise2. {¬p, r} Premise3. {¬q,r} Premise4. {¬q,s} Premise5. {¬r} Goal20Pure Literal EliminationA literal in a database is pure if and only if there is nocomplementary occurrence of the literal in thedatabase.A clause is superfluous if and only if it contains apure literal.Metatheorem: There is a resolution refutation of Δ ifand only if there is a resolution refutation from Δ inwhich all superfluous clauses are removed.1121Example1. {p, q} Premise2. {¬p, r} Premise3. {¬q,r} Premise4. {¬q,s} Premise5. {¬r} Goal22NoteThe removal of a superfluous clause may create newpure literals and new superfluous clauses.1. {p, q} p∨ q2. {¬p, r} p ⇒ r3. {¬q,r} q ⇒ r4. {¬q,s,t} q ⇒ s ∨ t5. {¬r} ¬r6. {¬t} ¬t1223StrategiesElimination Strategies (Constraints on clauses):Identical Clause EliminationTautology EliminationSubsumption EliminationPure Literal EliminationRestriction Strategies (Constraints on inferences):Unit RestrictionInput RestrictionLinear RestrictionSet of Support Restriction24Unit RestrictionA unit clause is a clause containing exactly one literal.Examples:{p}{¬p}Non-Examples:{}{p(x),q(a)}A unit resolution is one in which at least one of theparents is a unit clause.1325Examples1. {p,q}2. {¬p, r}3. {¬q, r}4. {¬q, s}5. {¬r}6. {q, r} 1,27. {p,r} 1,38. {p,s} 1,49. {¬p} 2, 510. {¬q} 3,511. {r} 3,612. {r,s} 4, 613. {q} 5,614. {r} 2, 715. {p} 5,716. {r,s} 2, 817. {q} 1,918. {r} 7,919. {s} 8,920. {p} 1,1021. {r} 6,1022. {} 5,1126Incompleteness of Unit Resolution1. {p, q} p ∨ q2. {p, ¬q} p ∨ ¬q3. {¬p, q} ¬p ∨ q4. {¬p, ¬q} ¬p ∨ ¬q1427Input RestrictionAn input resolution is one in which at least one of theparents is a member of the initial database (premise orgoal).28Input Restriction1. {p,q}2. {¬p, r}3. {¬q, r}4. {¬q, s}5. {¬r}6. {q, r} 1,27. {p,r} 1,38. {p,s} 1,49. {¬p} 2, 510. {¬q} 3,511. {r} 3,612. {r,s} 4, 613. {q} 5,614. {r} 2, 715. {p} 5,716. {r,s} 2, 817. {q} 1,918. {r} 7,919. {s} 8,920. {p} 1,1021. {r} 6,1022. {} 5,111529Incompleteness of Input RestrictionTheorem: Input resolution is not refutation complete.Argument: In propositional case, parents of emptyclause must both be units.Curious Fact: Unit Resolution and Input Resolutionwork in exactly the same cases.1. {p, q} p ∨ q2. {p, ¬q} p ∨ ¬q3. {¬p, q} ¬p ∨ q4. {¬p, ¬q} ¬p ∨ ¬q30Motivation for Linear Restriction1. {p, q} p ∨ q2. {p, ¬q} p ∨ ¬q3. {¬p, q} ¬p ∨ q4. {¬p, ¬q} ¬p ∨ ¬q5. {p} 1,26. {¬p} 3,47. {} 5,61631Elegant but
View Full Document