Gourt Home::Gourt :: Method of analytic tableaux
In proof theory, semantic tableaux provide a decision procedure for proving valid formulas, as well as, in some cases, the satisfiability of finite sets of formulas, of various logics. It is the most popular proof procedure for modal logics. Analytic tableaux are special kind of tableaux that do not have a "cut" rule—i.e. the only formulas occurring in a proof (i.e. tableau) are subformulas of the proved formula.
Although the fundamental idea behind the analytic tableau method can be seen to be 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 since the connection with proof theory has been made only in the last couple of 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 like multisets or lists or even trees of formulae. If there is such a rule for every logical connective then the procedure will eventually produce a set (multiset, list, tree) which consists only of atomic formulae and their negations, which cannot be broken down any further. Such a set (multiset, list, tree) 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 example of a tableau calculus for classical propositional logic. Tableau calculi for other logics can be obtained using very similar ideas.
If we write the classical conjunction "and" as & then the following rule can be considered a tableau rule:
(&): 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 BAnother 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 then 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:
Y, A & B (&)
Y, A, B
If we write the classical disjunction "or" as v then the following rule can be considered a tableau rule:
(v): 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:
(v) if the current node looks like (Y, A v B) then create two sibling child nodes that looks like (Y, A) and (Y, B) respectivelyGoing one step further we can drop the surrounding English prose and use | to create a pair of siblings and write the (v) rule as:
Y, A v B (v)
Y, A | Y, B
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 p's and q's 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:
Y, p, ~p (id)
- closed
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 v 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.
Classical propositional logic usually also contain a connective to capture logical implication. If we write this connective as -> then the formula (A -> B) stands for "A implies 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, else 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) v 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 negated normal form and it is possible to prove formally that every formula C of classical logic has a logically equivalent formula C' in negated normal form. That is, C is satisfiable if and only if C' is satisfiable.
The three rules (&), (v) 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.
The rules are actually enough 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.
Scientific research and efficient tableau procedures for automating deduction in many different logics is regularly reported in the Annual Conference on Theorem Proving with Analytic Tableaux and Related Methods which you can find by searching for TABLEAU 20xy or TABLEAUX 19xy where xy is the year of the conference. There is also a Journal of Automated Reasoning.
External links
- TABLEAUX: international conference on automated reasoning with analytic tableaux and related methods
"Method of analytic tableaux"