Method of analytic tableaux
From Wikipedia, the free encyclopedia
In proof theory, the semantic tableau is a decision procedure for sentential and related logics, and a proof procedure for formulas of first order logic. The tableau method can also determine the satisfiability of finite sets of formulas of various logics. It is the most popular proof procedure for modal logics (Girle 2000).
An analytic tableau has for each node a subformula of the formula at the origin. In other words, it is a tableau satisfying the subformula property.
Contents |
[edit] Introduction
For refutation tableaux, the objective is to show that the negation of a formula cannot be satisfied. There are rules for handling each of the usual connectives, starting with the main connective. In many cases, applying these rules causes the subtableau to divide into two. Quantifiers are instantiated. If any branch of a tableau leads to an evident contradiction, the branch closes. If all branches close, the proof is complete and the original formula is a logical truth.
Although the fundamental idea behind the analytic tableau method is derived from the cut-elimination theorem of structural proof theory, the origins of tableau calculi lie in the meaning (or semantics) of the logical connectives, as the connection with proof theory was made only in recent decades.
More specifically, a tableau calculus consists of a finite collection of rules with each rule specifying how to break down one logical connective into its constituent parts. The rules typically are expressed in terms of finite sets of formulae, although there are logics for which we must use more complicated data structures, such as multisets, lists, or even trees of formulas. Henceforth, "set" denotes any of {set, multiset, list, tree}.
If there is such a rule for every logical connective then the procedure will eventually produce a set which consists only of atomic formulae and their negations, which cannot be broken down any further. Such a set is easily recognizable as satisfiable or unsatisfiable with respect to the semantics of the logic in question. To keep track of this process, the nodes of a tableau itself are set out in the form of a tree and the branches of this tree are created and assessed in a systematic way. Such a systematic method for searching this tree gives rise to an algorithm for performing deduction and automated reasoning. Note that this larger tree is present regardless of whether the nodes contain sets, multisets, lists or trees.
We now consider the tableau calculus for classical propositional logic. Tableau calculi for other logics can be obtained using very similar ideas.
[edit] And
If we write the classical conjunction as '&', then the following rule can be considered a tableau rule for conjunction:
(&): If the current node contains a conjunctive formula (A & B) then create a single child node which is identical to the current node except that the single formula A & B is replaced by its two smaller constituent formulae A and B
Another way to say that a node contains a set X which itself contains a formula (A & B) is to write X as (Y, {A & B}) with Y standing for all the formulae in X other than (A & B), the {A & B} standing for the set containing the single formula (A & b), and comma standing for set union. If we also agree to drop the set braces, the rule for (&) can be written as:
(&) If the current node looks like (Y, A & B) then create a single child that looks like (Y, A, B)
Going one step further we can drop the surrounding English prose and write the 
rule as:
[edit] Or
If we write classical disjunction as ∨, then the following rule can be considered a tableau rule for disjunction:
(∨): If the current node contains a disjunctive formula (A v B) then create two sibling child nodes which are identical to the current node except that the single formula A v B is replaced by its smaller constituent formulae A in one child and B in the other child.
Or as:
(∨) If the current node looks like (Y, A v B) then create two sibling child nodes that look like (Y, A) and (Y, B) respectively.
Going one step further we can drop the surrounding English prose and use | to create a pair of siblings and write the (∨) rule as:
Finally, consider a set that consists of atomic formulae and their negations only. If we write the classical negation "not" as the symbol ~ then such a set can be written as {p0, p1, ..., pn, ~q1, ~q2, ... , ~qm} where we write the atomic formulae as ps and qs with subscripts.
If no atomic formula and its negation appears in this set then the set is classically satisfiable by assigning the truth value "true" to all its members. On the other hand, if some atomic formula and its negation appears in this set then no classical assignment can make all members of the set true simultaneously since it would assign "true" to both the atomic formula and its negation, which is impossible in classical logic.
We can capture these ideas with the following rule which simply acts to stop the process of rule applications and where we use p to stand for an arbitrary atomic formula and ~p to stand for its negation:
(id) If the current node looks like (Y, p, ~p), then mark it as closed.
Or more succinctly:
A tableau for a given finite set X is a finite (upside down) tree with root X in which all child nodes are obtained by applying the tableau rules. A branch in such a tableau is closed if its leaf node contains "closed". A tableau is closed if all its branches are closed. A tableau is open if at least one branch is not closed.
Here are two closed tableaux for the set X = {r0 & ~r0, p0 & ((~p0 ∨ q0) & ~q0)} with each rule application marked at the right hand side:
{r0 & ~r0, p0 & ((~p0 v q0) & ~q0)} {r0 & ~r0, p0 & ((~p0 v q0) & ~q0)}
--------------------------------------(&) ------------------------------------------------------------(&)
{r0 , ~r0, p0 & ((~p0 v q0) & ~q0)} {r0 & ~r0, p0, ((~p0 v q0) & ~q0)}
-------------------------------------(id) ----------------------------------------------------------(&)
closed {r0 & ~r0, p0, (~p0 v q0), ~q0}
-------------------------------------------------------------(v)
{r0 & ~r0, p0, ~p0, ~q0} | {r0 & ~r0, p0, q0, ~q0}
-------------------------- (id) ---------------------- (id)
closed closed
The left hand tableau closes after only one rule application while the right hand one misses the mark and takes a lot longer to close. Clearly, we would prefer to always find the shortest closed tableaux but it can be shown that one single algorithm that finds the shortest closed tableaux for all input sets of formulae cannot exist.
[edit] Conditional
Classical propositional logic usually has a connective to denote material implication. If we write this connective as →, then the formula (A→B) stands for "if A then B". It is possible to give a tableau rule for breaking down (A→B) into its constituent formulae. Similarly, we can give one rule each for breaking down each of ~(A & B) and ~(A v B) and ~~A and ~(A→B). Together these rules would give a terminating procedure for deciding whether a given set of formulae is simultaneously satisfiable in classical logic since each rule breaks down one formula into its constituents but no rule builds larger formulae out of smaller constituents. Thus we must eventually reach a node that contains only atoms and negations of atoms. If this last node matches (id) then we can close the branch, otherwise it remains open.
But note that the following equivalences hold in classical logic where (...) = (...) means that the left hand side formula is logically equivalent to the right hand side formula:
~(A & B) = ((~A) v (~B)) ~(A v B) = ((~A) & (~B)) ~~A = A ~(A→B) = (A&~B) (A → B) = ((~A) ∨ B).
If we start with an arbitrary formula C of classical logic, and apply these equivalence to replace the left hand sides with the right hand sides in C, and perform these operations repeatedly, then we will obtain a formula C' which is logically equivalent to C but which has the following property:
C' contains no implications, and ~ appears in front of atomic formulae only.
Such a formula is said to be in negation normal form and it is possible to prove formally that every formula C of classical logic has a logically equivalent formula C' in negation normal form. That is, C is satisfiable if and only if C' is satisfiable.
[edit] Summing up
The three rules (&), (∨) and (id) given above are then enough to decide if a given set X' of formulae in negated normal form are jointly satisfiable:
Just apply all possible rules in all possible orders until we find a closed tableau for X' or until we exhaust all possibilities and conclude that every tableau for X' is open.
In the first case, X' is jointly unsatisfiable and in the second the case the leaf node of the open branch gives an assignment to the atomic formulae and negated atomic formulae which makes X' jointly satisfiable. Classical logic actually has the rather nice property that we need to investigate only (any) one tableau completely: if it closes then X' is unsatisfiable and if it is open then X' is satisfiable. But this property is not generally enjoyed by other logics.
These rules suffice for all of classical logic by taking an initial set of formulae X and replacing each member C by its logically equivalent negated normal form C' giving a set of formulae X' . We know that X is satisfiable if and only if X' is satisfiable, so it suffices to search for a closed tableau for X' using the procedure outlined above.
By setting X = {~A} we can test whether the formula A is a tautology of classical logic:
If the tableau for {~A} closes then ~A is unsatisfiable and so A is a tautology since no assignment of truth values will ever make A false. Otherwise any open leaf of any open branch of any open tableau for {~A} gives an assignment that falsifies A.
Tableaux methods have had a considerable impact on the teaching of logic in philosophy departments (Jeffrey 1967 became a classic introductory text). On the other hand, they have had little impact on mathematical logic, despite Smullyan's (1995) endorsement.
[edit] References
Jeffrey is the easiest, Smullyan the hardest.
- Bostock, David, 1997. Intermediate Logic. Oxford Univ. Press.
- M D'Agostino, D Gabbay, R Haehnle, J Posegga (Eds), Handbook of Tableau Methods, Kluwer,1999.
- Girlie, Rod, 2000. Modal Logics and Philosophy. Teddington UK: Acumen.
- Richard Jeffrey, 1990 (1967). Formal Logic: Its Scope and Limits, 3rd ed. McGraw Hill.
- Raymond Smullyan, 1995 (1968). First Order Logic. Dover Publications.
- Journal of Automated Reasoning.
