StrategiesComputational LogicLecture 12Michael GeneserethSpring 20012PlanFirst Lecture:Pattern MatchingUnificationSecond Lecture:Relational Clausal FormResolution PrincipleResolution Theorem ProvingThird Lecture:True or False QuestionsFill in the Blank QuestionsResidueFourth Lecture:Strategies to enhance efficiency3Proof1. {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. Eliot5Proof 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,107StrategiesElimination 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 ∆ if and onlyif there is a resolution refutation from ∆ in which no clauseoccurs twice. (Obvious.)Upshot: If you generate a clause that is already in the proof, donot include it again.9Proof 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,211Tautology EliminationA tautology is a clause with a complementary pair of literals.{q,¬q}{p, q, r,¬q}{p(x), q(a,y),¬q(a,y), r(z)}Metatheorem: There is a resolution refutation of ∆ if and onlyif there is a resolution refutation from ∆ with tautologyelimination.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,713NoteNon-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}Premise15Propositional 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 and only ifthere is a resolution refutation from ∆ with PropositionalSubsumption.16NoteThe resolution of two clauses sometimes produces a clause thatsubsumes one of its parents.1. {p}Premise2. {¬r,q}Premise3. {r}Premise4. {¬p,¬q,¬r}Premise5. {¬q,¬r} 1,46. {¬r} 2,57. {} 3,617Relational SubsumptionA relational clause Φ subsumes Ψ if and only if there is asubstitution σ that, when applied to Φ, produces a clause Φσ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 ∆ if and onlyif there is a resolution refutation from ∆ with subsumption.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)}19Example 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 the database.A clause is superfluous if and only if it contains a pure literal.Metatheorem: There is a resolution refutation of ∆ if and onlyif there is a resolution refutation from ∆ in which allsuperfluous clauses are removed.21Example1. {p,q}Premise2. {¬p,r}Premise3. {¬q,r}Premise4. {¬q,s}Premise5. {¬r} Goal22NoteThe removal of a superfluous clause may create new pureliterals 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} ¬t23StrategiesElimination 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 the parents is aunit clause.25Examples1. {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∨ ¬q27Input RestrictionAn input resolution is one in which at least one of the parentsis a member of the initial database (premise or goal).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,1129Incompleteness of Input RestrictionTheorem: Input resolution is not refutation complete.Argument: In propositional case, parents of empty clause mustboth be units.Curious Fact: Unit Resolution and Input Resolution work inexactly 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,631Elegant but Non-Linear Proof{P,Q}{P,-Q}{-P,Q}{-P,-Q}{P}{-P}{}32Linear RestrictionA linear resolution is one in which one of the parents is aninput clause or a parent of the other clause.More specifically, the resolution can be restricted to those inwhich the resolution involves the same literal in the parent thatled to the child.Metatheorem:
View Full Document
Unlocking...