DOC PREVIEW
Stanford CS 157 - Ordered Resolution

This preview shows page 1-2-14-15-29-30 out of 30 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 30 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 30 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 30 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 30 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 30 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 30 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 30 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

Ordered ResolutionUnordered Propositional ResolutionExampleLarge Search SpaceIntuition for Ordered ResolutionClauses and ChainsOrdered Propositional ResolutionOrdered Relational ResolutionSmaller Search SpaceDoes Not Play Well With OthersSemi-Ordered ResolutionSlide 12ContrapositivesSlide 14Horn Clauses and Horn ChainsCompletenessSlide 17Slide 18Input ResolutionLinear ResolutionModel EliminationNormal and Reduced LiteralsReductionCancellationDroppingSlide 26Slide 27No Forward CancellationNotesSummaryOrdered ResolutionComputational Logic Lecture 13Michael Genesereth Autumn 20072Unordered Propositional ResolutionOrdinary resolution is unordered. The rule can be applied to any literal in either clause.The more opportunities for resolution, the larger the search space.€ {ϕ1,..., χ ,...,ϕm}{ψ1,...,¬ χ ,...,ψn}{ϕ1,...,ϕm,ψ1,...,ψn}3ExampleNegated Goal{p3,q3,r3}Premises{p3,p2} {q3,q2} {r3,r2}{p2,p1} {q2,q1} {r2,r1}{p1} {q1} {r1}4Large Search Space{¬p3,¬q3,¬r3} {¬p2,¬q3,¬r3} {¬p1,¬q3,¬r3}{¬p3,¬q3,¬r2} {¬p2,¬q3,¬r2} {¬p1,¬q3,¬r2}{¬p3,¬q3,¬r1} {¬p2,¬q3,¬r1} {¬p1,¬q3,¬r1}{¬p3,¬q2,¬r3} {¬p2,¬q2,¬r3} {¬p1,¬q2,¬r3}{¬p3,¬q2,¬r2}. {¬p2,¬q2,¬r2} {¬p1,¬q2,¬r2}{¬p3,¬q2,¬r1} {¬p2,¬q2,¬r1} {¬p1,¬q2,¬r1}{¬p3,¬q1,¬r3} {¬p2,¬q1,¬r3} {¬p1,¬q1,¬r3}{¬p3,¬q1,¬r2} {¬p2,¬q1,¬r2} {¬p1,¬q1,¬r2}{¬p3,¬q1,¬r1} {¬p2,¬q1,¬r1} {¬p1,¬q1,¬r1}5To derive empty clause, every literal must be eliminated.Idea: work on one literal till it is gone before starting to work on other literals.Intuition for Ordered Resolution{ ¬p3, ¬q3,¬r3}| | |¬p2¬q2¬r2| | |¬p1¬q1¬r16Clauses and ChainsA clause is a set of literals.{p,q,r}A chain is a sequence of literalsp,q,r7Note the order of the literals in the resolvent. Either way works, but you must be consistent.Ordered Propositional Resolution€ 〈χ,ϕ1,...,ϕm〉〈¬χ ,ψ1,...,ψn〉〈ϕ1,...,ϕm,ψ1,...,ψn〉8Ordered Relational Resolution€ 〈ϕ,ϕ1,...,ϕm〉〈¬ψ,ψ1,...,ψn〉〈ϕ1τ,...,ϕmτ,ψ1,...,ψn〉σwhere σ = mgu(ϕτ,ψ )where τ is a variable renaming on ϕNB : Still need factoring.9Smaller Search Space10. ¬〈 p3,¬q3,¬r3〉11. ¬〈 p2,¬q3,¬r3〉12. ¬〈 p1,¬q3,¬r3〉13. ¬〈 q3,¬r3〉14. ¬〈 q2,¬r3〉15. ¬〈 q1,¬r3〉16. ¬〈 r3〉17. ¬〈 r2〉18. ¬〈 r1〉19. 〈 〉1. 〈 p3,¬p2〉2. 〈p2,¬p1〉3. 〈p1〉4. 〈q3,¬q2〉5. 〈q2,¬q1〉6. 〈q1〉7. 〈r3,¬r2〉8. 〈r2,¬r1〉9. 〈r1〉10Does Not Play Well With OthersOrdered Resolution + Set of Support is not complete.Two Complete Answers and One Partial Answer:Semi-Ordered ResolutionContrapositivesHorn Restriction€ 1. 〈p,q〉 Premise2. 〈¬p,q〉 Premise3. 〈¬q〉 Goal11Semi-Ordered Resolution€ 〈ϕ1,...,ϕ ,...,ϕm〉〈¬ψ,ψ1,...,ψn〉〈ϕ1τ,...,ϕmτ,ψ1,...,ψn〉σwhere σ = mgu(ϕτ,ψ )where τ is a variable renaming on ϕNB : Still need factoring.12Example€ 1. 〈p,q〉 Premise2. 〈¬p,q〉 Premise3. 〈¬q〉 Goal4. 〈p〉 1,35. 〈¬p〉 2,36. 〈〉 4,513ContrapositivesA contrapositive of a chain is a permutation in which a different literal is placed at the front.Chain: p, q, rContrapositive: q, p, rContrapositive: r, p, qThe contrapositives of a chain are logically equivalent to the original chain.14Example€ 1. 〈p,q〉 Premise2. 〈q, p〉 Premise3. 〈¬p,q〉 Premise4. 〈q,¬ p〉 Premise5. 〈¬q〉 Goal6. 〈p〉 2,57. 〈¬p〉 4,58. 〈〉 6,715Horn Clauses and Horn ChainsA Horn clause is a clause containing at most one positive literal.A Horn chain is a chain containing at most one positive literal.Example: r,p,qExample: p,q,rExample: pNon-Example: q,r,pIn Horn chains, positive literals are usually put first.16CompletenessMetatheorem: If  consists entirely of Horn chains and all chains are ordered with positive literals, if any, first, then there is a resolution refutation of  if and only if there is a set of support refutation using ordered resolution.17Example1. 〈m〉 Premise2. 〈 p,¬m〉 Premise3. 〈q,¬m〉 Premise4. 〈r,¬p,¬q〉 Premise5. ¬〈 r〉 Goal6. ¬〈 p,¬q〉 4,57. ¬〈 m,¬q〉 2,68. ¬〈 q〉 1,79. ¬〈 m〉 3,810. 〈 〉 1,918Example€ 1. 〈p(art,bob)〉 Premise2. 〈p(art,bud)〉 Premise3. 〈p(bob,cal)〉 Premise4. 〈p(bud,coe)〉 Premise5. 〈g(x,z),¬ p(x, y),¬ p(y,z)〉 Premise6. 〈¬g(art,coe)〉 Goal7. 〈¬p(art, y),¬ p(y,coe)〉 5,68. 〈¬p(bud,coe)〉 2,79. 〈〉 4,819Input ResolutionAn input resolution is one in which at least one of the parents is a member of the initial database (premise or goal).Fcat: Input resolution is not complete.20Linear ResolutionA linear resolution is one in which one of the parents is an input clause or an ancestor of the other clause.More specifically, the resolution can be restricted to those in which the resolution involves the same literal in the parent that led to the child.Metatheorem: Linear Resolution is complete!!21Model EliminationModel Elimination is a variant of Ordered Resolution that incorporates the Linearity Restriction in the definition of the rules of inference.Using Model Elimination alone, it is possible to build a theorem prover that is sound and complete for all of Relational Logic.Moreover, it works with the Set of Support strategy and the Input Restriction!!!22Normal and Reduced LiteralsNormal Literals:pqReduced Literals:[p][q]Chains:p,q,[p],r23ReductionReductionExample€ 〈ϕ,ϕ1,...,ϕm〉〈ψ,ψ1,...,ψn〉〈ϕ1,...,ϕm,[ψ ],ψ1,...,ψn〉σwhere σ = mgu(¬ ϕ ,ψ )€ 〈g(x, z),¬ p(x, y),¬ p(y,z)〉〈¬g(a,v),¬ h(v)〉〈¬p(a, y),¬ p(y,v),[¬ g(a,v)],¬ h(v)〉24CancellationCancellationExample€ 〈ϕ,ϕ1,...,ϕm,[ψ ],ψ1,...,ψn〉〈ϕ1,...,ϕm,[ψ ],ψ1,...,ψn〉σwhere σ = mgu(¬ ϕ ,ψ )€ 〈g(x,b),¬ p(x, y),[¬ g(a,z)],¬ h(z)〉〈¬p(a, y),[¬ g(a,b)],¬ h(b)〉25DroppingDroppingExample€ 〈[ϕ ],ϕ1,...,ϕm〉〈ϕ1,...,ϕm〉€ 〈[¬ g(a,v)],¬ h(v)〉〈¬h(v)〉26Example1. 〈 p〉 Premise2. 〈q〉 Premise3. 〈r,¬p,¬q〉 Premise4. ¬〈 r〉 Goal5. ¬〈 p,¬q,[¬r]〉 Reduction:3,46. 〈[¬p],¬q,[¬r]〉 Reduction:1,57. ¬〈 q,[¬r]〉 Dropping:68. 〈[¬q],[¬r ]〉 Reduction:2,79. 〈[¬r]〉 Dropping:810. 〈 〉 Dropping:927Example€ 1. 〈p,q〉 Premise2. 〈r,¬ p〉


View Full Document

Stanford CS 157 - Ordered Resolution

Documents in this Course
Lecture 1

Lecture 1

15 pages

Equality

Equality

32 pages

Lecture 19

Lecture 19

100 pages

Epilog

Epilog

29 pages

Equality

Equality

34 pages

Load more
Download Ordered Resolution
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Ordered Resolution and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Ordered Resolution 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?