CS262 Logic and Verification Lecture 6: Semantic tableau
CS262 Logic and Verification 1 / 11
Semantic tableau and resolution
Copyright By PowCoder代写 加微信 powcoder
Two proof procedures for propositional logic: semantic tableau and resolution
Semantic tableau: closely connected to disjunctive normal form (DNF) Resolution: closely connected to conjunctive normal form (CNF)
Both systems are very well suited for automation; Assignment: implement a resolution theorem prover in Prolog
Both are refutation systems: To prove that a formula X is a tautology, we begin with ¬X and produce a contradiction
In the following we first talk about tableau, then about resolution
CS262 Logic and Verification 2 / 11
Semantic tableau
Proof takes the form of a tree, with nodes labelled by propositional formulas.
¬((x ∧ (y → (z ∨ w))) → (x ∨ y)) x ∧ (y → (z ∨ w))
y → (z ∨ w)
Think of each branch as a conjunction of the formulas on that branch, and think of the tree as the disjunction of all of its branches (disjunction of conjunctions; DNF)
CS262 Logic and Verification 3 / 11
Tableau expansion
In each step, select a branch and a non-literal formula N on that branch.
If N = ¬⊤, then extend the branch by a node labelled ⊥ at its end.
If N = ¬⊥, then extend the branch by a node labelled ⊤ at its end.
If N = ¬¬Z, then extend the branch by a node labelled Z at its end.
If N is an α-formula, then extend the branch by two nodes labelled α1,α2 (α-expansion) at its end.
If N is a β-formula, then add a left and right child to the final node of the branch, and label one of them β1 and the other one β2 (β-expansion).
Tableau expansion rules:
¬⊤ ¬⊥ ¬¬Z β α ⊥ ⊤ Z β1|β2 α1 α2
CS262 Logic and Verification
¬((p → (q → r)) → ((p ∨ s) → ((q → r) ∨ s)))
CS262 Logic and Verification 5 / 11
Closed tableau
A branch of a tableau is closed, if both X and ¬X occur on the branch for some formula X, or if ⊥ occurs on the branch.
If x and ¬x appear on a branch (where x is a variable), or if ⊥ appears, then the branch is atomically closed.
A tableau is (atomically) closed, if every branch is (atomically) closed. A tableau proof of X is a closed tableau for ¬X.
We write ⊢t X if X has a tableau proof.
CS262 Logic and Verification
Two tableau proofs of (p ∧ (q → (r ∨ s))) → (p ∨ q)
CS262 Logic and Verification 7 / 11
Tableau properties
Tableau proofs can be very short compared to truth tables: Consider X ∨ ¬X for some complicated formula X
Tableau method extends to first order logic (quantifiers), whereas truth tables do not
Tableau can be generalized to establish propositional consequences S |= X, not just tautologies |= X.
Tableau rules are non-deterministic: We have freedom in applying them. Different rules may produce proofs of different length.
CS262 Logic and Verification
Implementation
Reuse of formulas: How do we know when we should give up on a proof attempt? We can always try again something we have tried before, and maybe now it will work.
A tableau is strict, if no formula has had an expansion rule applied to it twice on the same branch.
Represent the tree as a list of lists (disjunction of conjunctions): Strictness rule allows us to remove an expanded formula from the list
With this, tableau expansion becomes identical to disjunctive normal form expansion
CS262 Logic and Verification 9 / 11
Implementation
So we could run the DNF expansion algorithm, and check for closure in the very end
We do not need to expand completely before checking for closure!
By being clever about when to check for closure and when to apply which expansion rule, we can shorten a proof considerably
There is considerable scope and necessity for heuristics
CS262 Logic and Verification 10 / 11
Soundness and completeness
Theorem: The tableau proof system is sound, i.e., if X has a tableau proof, then X is a tautology.
Theorem: The tableau proof system is complete, i.e., if X is a tautology, then the (strict) tableau system will terminate with a proof for it.
Equivalently, ⊢t X if and only if |= X .
First theorem follows from the correctness proof of our DNF expansion algorithm given before: Every expansion step produces a logically equivalent formula.
Proof of second theorem: not given here; requires more advanced tools.
CS262 Logic and Verification
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com