StrategiesPlanProofPoemProof as Produced by Two Finger MethodProof (continued)Slide 7Identical Clause EliminationProof With Identical Clause EliminationMotivation for Tautology EliminationTautology EliminationProof with TE and ICENoteMotivation for SubsumptionPropositional SubsumptionSlide 16Relational SubsumptionSlide 18Example for Pure Literal EliminationPure Literal EliminationExampleSlide 22Slide 23Unit RestrictionExamplesIncompleteness of Unit ResolutionInput RestrictionSlide 28Incompleteness of Input RestrictionMotivation for Linear RestrictionElegant but Non-Linear ProofLinear RestrictionNon-ExampleSlide 34Linear ProofIntuition for Set of SupportSet of Support RestrictionSlide 38Combinations of StrategiesStrategiesComputational Logic Lecture 12Michael Genesereth Autumn 20072PlanFirst 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, …)3Proof1. {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 only if there is a resolution refutation from in which no clause occurs twice. (Obvious.)Upshot: If you generate a clause that is already in the proof, do not 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 only if there is a resolution refutation from with tautology 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,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 if there is a resolution refutation from with Propositional Subsumption.16NoteThe resolution of two clauses sometimes produces a clause 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,617Relational SubsumptionA relational clause subsumes if and only if there is a substitution that, when applied to , produces a clause that is a subset of .{p(a,b), q(c)}{p(x,y)}Why:{p(x,y)}{xa,yb} = {p(a,b)} {p(a,b), q(c)}Metatheorem: There is a resolution refutation of if and only if 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} Premis e2. {¬p,r} Premise3. {¬q,r} Premis e4. {¬q,s} Premise5. {¬r} Goal20Pure Literal EliminationA literal in a database is pure if and only if there is no complementary 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 only if there is a resolution refutation from in which all superfluous clauses are removed.21Example1. {p,q} Premis e2. {¬p,r} Premise3. {¬q,r} Premis e4. {¬q,s} Premise5. {¬r} Goal22NoteThe removal of a superfluous clause may create new pure 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} ¬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 a unit 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 parents is 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}
View Full Document
Unlocking...