Method Of Analytic Tableaux

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 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 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) respectively

Information About

Method Of Analytic Tableaux