EpilogComputational LogicLecture 14Michael GeneserethSpring 20022OverviewEpilog is a theorem prover for Relational Logic. It is soundand complete. It is at least as efficient as Model Elimination,and it is arguably more efficient. It is somewhat more intuitivethan ordinary Resolution.Features:Rule Form instead of Clausal FormBackward ChainingIterative Deepening rather than Breadth-First Search3Rule FormRule Form is the same as clausal form except that clauses areexpressed using “rule” syntax rather than set notation.There are two cases.Premise form is used for premises.Question form is used for desired conclusions.4PremisesPremises are expressed as rules.Note that 〈ψ,¬ϕ1,…,¬ϕn〉 is equivalent to (ψ ⇐ ϕ1 ∧ … ∧ ϕn).〈p〉 p ⇐〈¬p〉 ¬p ⇐〈r,¬p,¬q〉 r ⇐ p∧ q5ConclusionsConclusions are expressed as questions.Note that 〈¬ϕ1,…,¬ϕn〉 is equivalent to (¬ϕ1∨…∨¬ϕn).Note that (¬ϕ1∨…∨¬ϕn) is equivalent to ¬(ϕ1∧…∧ϕn).〈p〉 ¬p?〈¬p〉 p?〈¬p,¬q,r〉 p∧ q ∧ ¬r?6Backward ChainingBackward Chaining is the same as reduction except that itworks on rule form rather than clausal form.ϕ ⇐ϕ1∧...∧ϕmψ ∧ψ1∧...∧ψn?ϕ1∧...∧ϕm∧[ψ]∧ψ1∧...∧ψn?σwhere σ = mgu(ϕ,ψ )Reduced literals are retained only for non-Horn premises.Cancellation and Dropping are analogous.7Example1. m ⇐Premise2. p ⇐ mPremise3. q ⇐ mPremise4. r ⇐ p∧ qPremise5. r? Goal6. p∧ q? 4,57. m ∧ q? 2,68. q? 1,79. m? 3,810. ? 1,98Example9. p∧ q? Goal10. ¬q ∧[p]∧ q? 1,911. ¬p∧[¬q]∧[p]∧ q? 4,1012. [¬q]∧[p]∧ q? 1113. [p]∧ q? 1214. q? 1315. p∧[q]? 6,1416. ¬q ∧[p]∧[q]? 1,1517. [p]∧[q]? 1618. [q]? 1719. ? 181. p ⇐ ¬q p∨ q2. q ⇐ ¬p p∨ q3. p ⇐ q p∨ ¬q4. ¬q ⇐ ¬p p ∨ ¬q5. ¬p ⇐ ¬q ¬p∨ q6. q ⇐ p ¬p∨ q7. ¬p ⇐ q ¬(p ∧ q)8. ¬q ⇐ p ¬(p ∧ q)9Answer ExtractionTo extract answers start with definition of goal relation ratherthan question.p(x,y) ∧ q(y,z)?goal(x,z) ⇐ p(x, y) ∧ q(y,z)10Answer Extraction Ruleϕ ⇐ϕ1∧...∧ϕmγ ⇐ψ ∧ψ1∧...∧ψn(γ ⇐ϕ1∧...∧ϕm∧[ψ]∧ψ1∧...∧ψn)σwhere σ = mgu(ϕ,ψ )where γ is a goal literal11Example1. m(a,a) ⇐Premise2. p(x,y)⇐ m(x,y)Premise3. q(x, y) ⇐ m(x,y)Premise4. r(x,z) ⇐ p(x, y) ∧ q(y,z)Premise5. goal(x,z) ⇐ r(x,z) Goal6. goal(x,z) ⇐ p(x,y)∧ q(y,z) 4,57. goal(x,z) ⇐ m(x,y) ∧ q(y,z) 2,68. goal(a,z) ⇐ q(a,z) 1,79. goal(a,z) ⇐ m(a,z) 3,810. goal(a,a) ⇐ 1,912Troubling Example1. p(a) ⇐ ¬p(b) p(a)∨ p(b)2. p(b) ⇐ ¬p(a) p(a)∨ p(b)3. goal(x) ⇐ p(x) Goal4. ¬p(x) ⇐ ¬goal(x) Goal5. goal(a) ⇐ ¬p(b)∧[p(a)] 1,36. goal(a) ⇐ ¬goal(b) ∧[¬p(b)]∧[p(a)] 4,513Multiple Goal Ruleγ ⇐ ¬γ ' ∧ψ ∧ψ1∧...∧ψnγ ∨γ ' ⇐ψ ∧ψ1∧...∧ψnwhere γ and γ ' are goal literals14Example1. p(a) ⇐ ¬p(b) p(a)∨ p(b)2. p(b) ⇐ ¬p(a) p(a)∨ p(b)3. goal(x) ⇐ p(x) Goal4. ¬p(x) ⇐ ¬goal(x) Goal5. goal(a) ⇐ ¬p(b)∧[p(a)] 1,36. goal(a) ⇐ ¬goal(b) ∧[¬p(b)]∧[p(a)] 4,57. goal(a) ∨ goal(b) ⇐[¬p(b)]∧[p(a)] 68. goal(a) ∨ goal(b) ⇐[p(a)] 79. goal(a) ∨ goal(b) ⇐ 815Search SpaceQuestion:a?Premisesa ⇐ b a ⇐ c a ⇐ db ⇐ e c ⇐ g d ⇐ ib ⇐ f c ⇐ h d ⇐ j16Search SpaceachgdjibfeGiven the Set of Support Restriction and input restriction, thesearch space looks like a simple tree or graph.There are different schedules for searching the tree or graph.17Breadth First Searcha b c d e f g h i jachgdjibfeAdvantage: Finds shortest pathDisadvantage: Saves lots of intermediate information18Depth First Searchachgdjibfea b e f c g h d i jAdvantage: Small intermediate storageDisadvantage: Susceptible to garden pathsDisadvantage: Susceptible to infinite loops19Time ComparisonAnalysis for branching 2 and depth d and solution at depth kTime BestWorstDepth k 2d− 2d−kBreadth 2k−12k−120Time ComparisonAnalysis for branching b and depth d and solution at depth k.Time BestWorstDepth kbd− bd−kb−1Breadthbk−1−1b −1+1bk−1b−121Space ComparisonWorst Case Space Analysis for search depth d and depth k.Space Binary GeneralDepth d (b−1)× (d −1) +1Breadth 2k−1bk−122Iterative DeepeningRun depth-limited search repeatedly,starting with a small initial depth,incrementing on each iteration,until success or run out of alternatives.23Exampleachgdjibfeaa b c da b e f c g h d i jAdvantage: Small intermediate storageAdvantage: Finds shortest pathAdvantage: Not susceptible to garden pathsAdvantage: Not susceptible to infinite loops24Time ComparisonDepthIterativeDepth1 1 12 4 33 11 74 26 155 57 31n 2n+1− n − 2 2n−125General ResultTheorem: The cost of iterative deepening search is b/(b-1) timesthe cost of depth-first search (where b is the branching factor).See Korf.26Ease of Understanding of Proof Process1. m ⇐Premise2. p ⇐ mPremise3. q ⇐ mPremise4. r ⇐ p∧ qPremise5. r? Goal6. p∧ q? 4,57. m ∧ q? 2,68. q? 1,79. m? 3,810. ? 1,9Call: r?Call: p?Call: m?Exit: mExit: pCall: q?Call: m?Exit: mExit: qExit: rDepth-First Search supports tracing and debugging.Highly important on problems with many rules.27Ease of Understanding of Proof Process1. p(a) ⇐2. p(b) ⇐3. q(b) ⇐4. r(x) ⇐ p(x) ∧ q(x)5. r(x)?Call: r(x)?Call: p(x)?Exit: p(a)Call: q(a)?Fail: q(a)?Redo: p(x)?Exit: p(b)Call: q(b)?Exit: q(b)?Exit: r(b)28Implementation NotesIn the implementation of Epilog, question literals, reducedliterals, and goal literals are kept in separate variables. Thisavoids cluttering chains and thereby simplifies derivations.Variables are not plugged in along the way but rather are keptin binding lists. This saves wasteful copying.In conjunctive questions, e.g. p(x) ∧ q(x), solutions to earlyliterals, e.g. p(x) are pipelined to later literals, e.g. q(x), ratherthan being computed up front. This circumvents infinite loopsin cases where there are infinitely many solutions.29Related SystemsProlog (David Warren)Horn Clauses onlyDepth-First Search means potential for infinite loopsNo occur check in unifierProlog Technology Theorem Prover (Mark Stickel)essentially the same as
View Full Document
Unlocking...