New version page

Stanford CS 157 - Strategies

Pages: 20
Documents in this Course

16 pages

36 pages

42 pages

42 pages

19 pages

17 pages

26 pages

35 pages

23 pages

16 pages

21 pages

32 pages

30 pages

41 pages

37 pages

15 pages

16 pages

20 pages

38 pages

25 pages

22 pages

100 pages

20 pages

21 pages

15 pages

15 pages

18 pages

17 pages

40 pages

16 pages

32 pages

39 pages

23 pages

25 pages

40 pages

17 pages

40 pages

30 pages

41 pages

22 pages

3 pages

36 pages

39 pages

17 pages

50 pages

39 pages

57 pages

34 pages

26 pages

32 pages

20 pages

16 pages

30 pages

39 pages

20 pages

34 pages

50 pages

42 pages

15 pages

34 pages

42 pages

100 pages

34 pages

28 pages

50 pages

17 pages

17 pages

29 pages

20 pages

17 pages

32 pages

19 pages

34 pages

36 pages

21 pages

16 pages

17 pages

36 pages

15 pages

100 pages

40 pages

30 pages

32 pages

34 pages

50 pages

40 pages

46 pages

18 pages

22 pages

32 pages

32 pages

Unformatted text preview:

1StrategiesComputational 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, …)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.

View Full Document