CS262 Logic and Verification Lecture 7: Resolution
CS262 Logic and Verification 1 / 14
Propositional resolution
Copyright By PowCoder代写 加微信 powcoder
Tableau proofs ↔ DNF Resolution proofs ↔ CNF
Tableau proofs presented as trees: Each branch is a conjunction, tree is the disjunction of its branches
Trees are not convenient for resolution: We use the standard representation ⟨[. . .], [. . .], . . .⟩, one disjunction on each line.
CS262 Logic and Verification
Resolution expansion
In each step, select a disjunction and a non-literal formula N in it.
If N = ¬⊤, then append a new disjunction where N is replaced by ⊥.
If N = ¬⊥, then append a new disjunction where N is replaced by ⊤.
If N = ¬¬Z, then append a new disjunction where N is replaced by Z.
If N is an α-formula, then append two new disjunctions, one in which N is replaced by α1, and one in which it is replaced by α2 (α-expansion).
If N is a β-formula, then append a new disjunction where N is replaced by β1,β2 (β-expansion).
Resolution expansion rules:
¬⊤ ¬⊥ ¬¬Z β α ⊥ ⊤ Z β1 α1|α2
CS262 Logic and Verification 3 / 14
1. [p↓(q∧r)]
2. [¬(q ∨ (p → q))]
CS262 Logic and Verification 4 / 14
Strict resolution
A sequence of resolution expansion applications is strict, if every disjunction has at most one resolution expansion rule applied to it.
Intuitively: no formula reuse
As with tableau, strict version suits itself for implementation: Remove formula from list after applying an expansion rule to it.
With this, resolution expansion becomes identical to conjunctive normal form expansion
CS262 Logic and Verification
Resolution rule
For resolution, we need yet another rule of a different nature, the resolution rule.
Suppose D1 and D2 are two disjunctions, with X occuring in D1 and ¬X in D2. Let D be the result of the following:
delete all occurences of X from D1 delete all occurences of ¬X from D2 combine the resulting disjunctions
Special case: If a disjunction contains ⊥, delete all occurences of ⊥, and call the resulting disjunction the trivial resolvent.
CS262 Logic and Verification 6 / 14
Resolution rule
D is the result of resolving D1 and D2 on X. D is the resolvent of D1 and D2, and X is the formula being resolved on. If X is atomic, then this is an atomic application of the resolution rule.
1. [p,q→r] 1. [a∧b] 1. [p,q↑r,⊥] 2. [a∧b,¬p] 2. [¬(a∧b)] ? ??
Justification of the resolution rule: ⟨[X,Y],[¬X,Z]⟩ = ⟨[X,Y],[¬X,Z],[Y,Z]⟩
CS262 Logic and Verification 7 / 14
Resolution proof
A resolution expansion is closed, if it contains the empty clause [ ]. A resolution proof for X is a closed resolution expansion for ¬X. We write ⊢r X if X has a resolution proof.
CS262 Logic and Verification 8 / 14
Resolution proof for ((p ∧ q) ∨ (r → s)) → ((p ∨ (r → s)) ∧ (q ∨ (r → s))):
1. [¬(((p∧q)∨(r →s))→((p∨(r →s))∧(q∨(r →s))))] 2. [(p ∧ q) ∨ (r → s)]
3. [¬((p∨(r →s))∧(q∨(r →s)))]
4. [p∧q,r →s]
5. [¬(p∨(r →s)),¬(q∨(r →s))] 6. [p,r → s]
7. [q,r → s]
8. [¬p,¬(q∨(r →s))]
9. [¬(r →s),¬(q∨(r →s))] 10. [¬p,¬q]
11. [¬p,¬(r → s)]
12. [¬(r → s),¬q]
13. [¬(r → s),¬(r → s)] 14. [r → s,¬p]
15. [r → s,r → s]
CS262 Logic and Verification
Proof steps:
α-expansion on 1. creates 2.+3.
β-expansion on 2. creates 4.
β-expansion on 3. creates 5.
α-expansion on 4. creates 6.+7.
α-expansion on 5. creates 8.+9.
α-expansion on 8. creates 10.+11. α-expansion on 9. creates 12.+13.
resolving on q in 7. and 10. creates 14. resolving on p in 6. and 14. creates 15. resolving on r → s in 13. and 15. creates 16.
CS262 Logic and Verification 10 / 14
Resolution properties
Resolution method extends to first order logic (quantifiers) Resolution can be generalized to establish propositional consequences
S |= X, not just tautologies |= X.
Resolution rules are non-deterministic: We have freedom in applying them.
Different rules may produce proofs of different length.
CS262 Logic and Verification 11 / 14
Soundness and completeness
Theorem: The resolution proof system is sound, i.e., if X has a resolution proof, then X is a tautology.
Theorem: The resolution proof system is complete, i.e., if X is a tautology, then the resolution system will terminate with a proof for it, even if if all resolution rule applications are atomic or trivial, and come after all resolution expansion steps.
Equivalently, ⊢r X if and only if |= X .
First theorem follows from the correctness proof of our CNF expansion algorithm given before. Also argued that resolution rule produces a semantically equivalent formula.
Proof of second theorem not given here; requires more advanced tools.
CS262 Logic and Verification
Propositional consequence
Recall the definition of propositional consequence S |= X .
S-introduction rule for tableau: Any formula Y ∈ S can be added to the end of any tableau branch. We write S ⊢t X if there is a closed tableau for ¬X allowing the S-introduction rule for tableau.
S-introduction rule for resolution: For any formula Y ∈ S, the line [Y ] can be added as a line to a resolution expansion. We write S ⊢r X if there is a closed resolution expansion for ¬X, allowing the S-introduction rule for resolution.
Theorem (Strong soundness and completeness): For any set S of propositional formulas and any formula X , we have S |= X if and only if S⊢t X ifandonlyifS⊢r X.
CS262 Logic and Verification 13 / 14
Prove {p → q, q → r } |= ¬(¬r ∧ p) via tableau and resolution.
CS262 Logic and Verification 14 / 14
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com