Stanford CS 157 - Propositional Resolution

Unformatted text preview:

Propositional ResolutionAxiom Schema InstancesSlide 3Clausal FormSlide 5Empty SetsConversion to Clausal FormSlide 8ExampleSlide 10Resolution PrincipleIssuesSlide 13Special CasesIncompleteness?AnswerSlide 17Slide 18Slide 19Soundness and CompletenessTwo Finger MethodTwo Finger Method in OperationTFM With Identical Clause EliminationTFM With ICE, Complement DetectionTerminationDecidability of Propositional EntailmentHorn ClausesComplexityExample for DPDavis Putnam ProcedureExample Without DPExample With DPMotivation for DPLLDavis Putnam Logemann LovelandSimplificationComparisonsCoin LogicSlide 38Propositional ResolutionComputational Logic Lecture 4Michael Genesereth Autumn 20072Axiom Schema Instances   (  )p  (p  p) p  (p  p  p) p  (p  p  p)p  (q  p) p  (p  q  p) p  (p  q  p)p  (r  p) p  (p  r  p) p  (p  r  p) q  (p  q) … ...q  (q  q)q  (r  q)r  (p  r)r  (q  r)r  (r  r)Proofs may be short, but many alternatives to consider.3Propositional ResolutionPropositional resolution is a rule of inference.Using propositional resolution alone (without axiom schemata or other rules of inference), it is possible to build a theorem prover that is sound and complete for all of Propositional Logic.The search space using propositional resolution is much smaller than for Modus Ponens and the Standard Axiom Schemata.4Clausal FormPropositional resolution works only on expressions in clausal form.Fortunately, it is possible to convert any set of propositional calculus sentences into an equivalent set of sentences in clausal form.5Clausal FormA literal is either an atomic sentence or a negation of an atomic sentence.p, pA clausal sentence is either a literal or a disjunction of literals.p, p, p  qA clause is a set of literals.{p}, {p}, {p,q}6Empty SetsThe empty clause {} is unsatisfiable.Why? It is equivalent to an empty disjunction.7Conversion to Clausal Formϕ1⇒ ϕ2→ ¬ϕ1∨ϕ2ϕ1⇐ ϕ2→ ϕ1∨¬ϕ2ϕ1⇔ ϕ2→ (¬ϕ1∨ϕ2) ∧(ϕ1∨¬ϕ2)¬¬ϕ → ϕ¬(ϕ1∧ϕ2) → ¬ϕ1∨¬ϕ2¬(ϕ1∨ϕ2) → ¬ϕ1∧¬ϕ2Implications Out:Negations In:8Conversion to Clausal FormDistributionOperators Out€ ϕ1∨(ϕ2∧ϕ3) → (ϕ1∨ϕ2)∧(ϕ1∨ϕn)(ϕ1∧ϕ2)∨ϕ3→ (ϕ1∨ϕ3)∧(ϕ2∨ϕ3)ϕ ∨(ϕ1∨...∨ϕn) → (ϕ ∨ϕ1∨...∨ϕn)(ϕ1∨...∨ϕn)∨ϕ → (ϕ1∨...∨ϕn∨ϕ )ϕ ∧(ϕ1∧...∧ϕn) → (ϕ ∧ϕ1∧...∧ϕn)(ϕ1∧...∧ϕn)∧ϕ → (ϕ1∧...∧ϕn∧ϕ )ϕ1∨...∨ϕn→ {ϕ1,...,ϕn}ϕ1∧...∧ϕn→ ϕ1,...,ϕn9Exampleg∧(r ⇒ f)I g∧(¬r ∨ f)N g∧(¬r ∨ f)D g∧(¬r ∨ f)O {g}{¬r, f}10Example¬(g∧(r ⇒ f))I ¬(g∧(¬r ∨ f ))N ¬g∨¬(¬r ∨ f))¬g∨(¬¬r ∧¬f)¬g∨(r ∧¬f )D (¬g∨r) ∧(¬g∨¬f)O {¬g,r}{¬g,¬f}11Resolution PrincipleGeneral:Example:{ϕ1,...,χ,...,ϕm}{ψ1,...,¬χ,...,ψn}{ϕ1,...,ϕm,ψ1,...,ψn}{p,q}{¬p,r}{q,r}12IssuesCollapseSingletons{¬p,q}{p,q}{q}{¬p,q}{p}{q}{p}{¬p}{}13IssuesMultiple ConclusionsSingle Application OnlyWrong!!{p,q}{¬p,¬q}{p,¬p}{q,¬q}{p,q}{¬p,¬q}{}14Special CasesModus Ponens Modus Tolens Chainingp⇒ qpqp⇒ q¬q¬pp⇒ qq⇒ rp⇒ r{¬p,q}{¬q,r}{¬p,r}{¬p,q}{¬q}{¬p}{¬p,q}{p}{q}15Incompleteness?Propositional Resolution is not generatively complete.We cannot generate p  (q  p) using propositional resolution. There are no premises. Consequently, there are no conclusions.16AnswerThis apparent problem disappears if we take the clausal form of the premises (if any) together with the negated goal and try to derive the empty clause.General Method: To determine whether a set  of sentences logically entails a sentence , rewrite {} in clausal form and try to derive the empty clause using the resolution rule of inference.17Example¬(p⇒ (q⇒ p))I ¬(¬p∨¬q∨ p)N ¬¬p∧¬¬q∧¬pp∧q∧¬pD p∧q∧¬pO {p}{q}{¬p}18ExampleIf Mary loves Pat, then Mary loves Quincy. If it is Monday, Mary loves Pat or Quincy. Prove that, if it is Monday, then Mary loves Quincy.1. {¬p,q} Premise2. {¬m, p,q} Premise3. {m} Negated Goal4. {¬q} Negated Goal5. {p,q} 3,26. {q} 5,17. {} 6,419ExampleHeads you win. Tails I lose. Show that you always win.1. {¬h,y} Premise2. {¬t,¬m} Premise3. {h,t} Premise4. {¬h,¬t} Premise5. {m,y} Premise6. {¬m,¬y} Premise7. {¬y} Negated Goal8. {t,y} 3,19. {¬m,y} 8,210. {y} 9,511. {} 10,720Soundness and CompletenessA sentence is provable from a set of sentences by propositional resolution if and only if there is a derivation of the empty clause from the clausal form of {}.Theorem: Propositional Resolution is sound and complete, i.e.  |=  if and only if  |- .21Two Finger Methodfunction tfm () ;  is a linked list of clauses {var fast  ; var slow  ; do {if slow = [] then return failure;   concat(, resolvents(first(fast),first(slow))); if {}   then return ; if fast=slow then {fast  ; slownext(slow)} else fastnext(fast)}}function resolvents(1,2) {1 {}2 {} | 1 and 2}  {1 {}2 {} | 1 and 2}22Two Finger Method in Operation1. {p,q} Premise2. {¬p,r} Premise3. {¬q,r} Premise4. {¬r} Premise5. {q,r} 1,26. {p,r} 1,37. {¬p} 2,48. {¬q} 3,49. {r} 3,510. {q} 4,511. {r} 2,612. {p} 4,613. {q} 1,714. {r} 6,715. {p} 1,816. {r} 5,817. {} 4,923TFM With Identical Clause Elimination1. {p,q} Premise2. {¬p,r} Premise3. {¬q,r} Premise4. {¬r} Premise5. {q,r} 1,26. {p,r} 1,37. {¬p} 2,48. {¬q} 3,49. {r} 3,510. {q} 4,511. {p} 4,612. {} 4,924TFM With ICE, Complement Detection1. {p,q} Premise2. {¬p,r} Premise3. {¬q,r} Premise4. {¬r} Premise5. {q,r} 1,26. {p,r} 1,37. {¬p} 2,48. {¬q} 3,49. {r} 3,510. {} 4,925TerminationTheorem: There is a resolution derivation of a conclusion from a set of premises if and only if there is a derivation using the two finger method.Theorem: Propositional resolution using the two-finger method always terminates.Proof: There are only finitely many clauses that can be constructed from a finite set of logical constants.26Decidability of Propositional EntailmentPropositional resolution is a decision procedure for Propositional Logic. Logical entailment for Propositional Logic is decidable.Sadly, the problem in general is NP-complete.27Horn ClausesA Horn clause is a


View Full Document

Stanford CS 157 - Propositional 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 Propositional 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 Propositional 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 Propositional 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?