Ordered ResolutionUnordered ResolutionExampleLarge Search SpaceIntuition for Ordered ResolutionClauses and ChainsSlide 7Smaller Search SpaceDoes Not Play Well With OthersSemi-Ordered ResolutionSlide 11ContrapositivesSlide 13Horn Clauses and Horn ChainsCompletenessSlide 16Input ResolutionLinear ResolutionModel EliminationNormal and Reduced LiteralsModel Elimination RulesSlide 22Slide 23No Forward CancellationSummaryOrdered ResolutionComputational Logic Lecture 13Michael Genesereth Spring 20052Unordered ResolutionOrdinary resolution is unordered. The rule can be applied to any literal in 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 first 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 literalsp,q,r7Ordered Resolution〈ϕ,ϕ1,...,ϕm〉¬〈 ψ ,ψ1,...,ψn〉〈ϕ1,...,ϕm,ψ1,...,ψn〉σwhere σ =mgu(ϕ,ψ )8Smaller 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〉9Does Not Play Well With OthersOrdered Resolution + Set of Support is not complete.Two Complete Answers and One Partial Answer:Semi-Ordered ResolutionContrapositivesHorn Restriction1. 〈 p,q〉 Premise2. ¬〈 p,q〉 Premise3. ¬〈 q〉 Goal10Semi-Ordered Resolution〈ϕ1,...,ϕ,...,ϕm〉〈ψ ,ψ1,...,ψn〉〈ϕ1,...,ϕm,ψ1,...,ψn〉σwhere σ =mgu(¬ϕ,ψ )11Example1. 〈 p,q〉 Premise2. ¬〈 p,q〉 Premise3. ¬〈 q〉 Goal4. 〈 p〉 1,35. ¬〈 p〉 2,36. 〈 〉 4,512ContrapositivesA contrapositive of a chain is a permutation in which a different literal is placed at the front.Chain: p,q,rContrapositive: q,p,rContrapositive: r,p,qThe contrapositives of a chain are logically equivalent to the original chain.13Example1. 〈 p,q〉 Premise2. 〈q,p〉 Premise3. ¬〈 p,q〉 Premise4. 〈q,¬p〉 Premise5. ¬〈 q〉 Goal6. 〈 p〉 2,57. ¬〈 p〉 4,58. 〈 〉 6,714Horn 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,qExample: p,q, rExample: pNon-Example: q,r,pIn Horn chains, positive literals are usually written first.15CompletenessMetatheorem: If consists entirely of Horn chains and all chains are ordered with positive literals first, then there is a resolution refutation of if and only if there is a set of support refutation using ordered resolution.16Example1. 〈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,917Input Resolution1. {p,q} Premise2. {p,¬q} Premise3. {¬p,q} Premise4. {¬p,¬q} Goal5. {p} 1,26. {q} 1,37. {p,¬p} 2,38. {q,¬q} 2,39. {¬q} 2,410. {¬p} 3,418Linear Resolution1. 〈 p,q〉 Premise2. 〈q,p〉 Premise3. ¬〈 p,q〉 Premise4. 〈q,¬p〉 Premise5. ¬〈 q〉 Goal6. 〈 p〉 2,57. ¬〈 p〉 4,58. 〈 〉 6,71. 〈 p,q〉 Premise2. 〈q,p〉 Premise3. ¬〈 p,q〉 Premise4. 〈q,¬p〉 Premise5. ¬〈 q〉 Goal6. 〈 p〉 2,57. 〈q〉 3,68. 〈 〉 5,7Nonlinear Linear19Model 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!!!20Normal and Reduced LiteralsNormal Literals:pqReduced Literals:[p][q]Chains:p,q,[p],r21Model Elimination RulesReductionCancellationDropping〈ϕ,ϕ1,...,ϕm〉〈ψ ,ψ1,...,ψn〉〈ϕ1,...,ϕm,[ψ ],ψ1,...,ψn〉σwhere σ =mgu(¬ϕ,ψ )〈[ϕ],ϕ1,...,ϕm〉〈ϕ1,...,ϕm〉〈ϕ,ϕ1,...,ϕm,[ψ ],ψ1,...,ψn〉〈ϕ1,...,ϕm,[ψ ],ψ1,...,ψn〉σwhere σ =mgu(¬ϕ,ψ )22Example1. 〈 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:923Example1. 〈 p,q〉 Premise2. 〈 p,¬q〉 Premise3. ¬〈 p,q〉 Premise4. ¬〈 p,¬q〉 Goal5. 〈q,[¬p],¬q〉 Reduction:1,46. 〈 p,[q],[¬p],¬q〉 Reduction:2,57. 〈[q],[¬p],¬q〉 Cancellation:68. 〈[¬p],¬q〉 Dropping:79. ¬〈 q〉 Dropping:810. 〈 p,[¬q]〉 Reduction:1,911. 〈q,[p],[¬q]〉 Reduction:3,1012. 〈[p],[¬q]〉 Cancellation:1113. 〈[¬q]〉 Dropping:1214. 〈 〉 Dropping:1324No Forward Cancellation1. 〈 p,q〉 Premise2. ¬〈 q,¬r〉 Premise3. 〈r〉 Premise4. ¬〈 p,¬q〉 Goal5. 〈q,[¬p],¬q〉 Reduction:1,46. ¬〈 r,[q],[¬p],¬q〉 Reduction:2,57. 〈[q],[¬p],¬q〉 Reduction:3,68. 〈[q],[¬p]〉 Cancellation:7 Wrong!!9. 〈[¬p]〉 Dropping:810. 〈 〉 Dropping:925SummaryOrdered Resolution with FactoringComplete without strategiesIncompatible with Set of SupportIncompatible with Input RestrictionSemi-Ordered Resolution and/or ContrapositivesCompleteWorks with Set of SupportIncompatible with Input RestrictionModel EliminationCompleteWorks with Set of SupportWorks with Input
View Full Document
Unlocking...