Editing Method of analytic tableaux (section)

=== General method ===
A tableau checks whether a given set of formulae is satisfiable or not. It can be used to check either validity or entailment: a formula is valid if its negation is unsatisfiable, and formulae <math>A_1,\ldots,A_n</math> imply <math>B</math> if <math>\{A_1,\ldots,A_n,\neg B\}</math> is unsatisfiable.

[[File:Prop-tableau-2.svg|thumb|100px|(a⋁¬b)⋀b generates a⋁¬b and b]]
For any formulae <math>X</math>, <math>Y</math> the following facts hold:  
* If a [[logical conjunction|conjunction]]<math>X \land Y</math><br/>{{spaces|4}}is true, then <math>X</math>, <math>Y</math> are both true;<br/>{{spaces|4}}is false, then either <math>X</math> is false or <math>Y</math> is false.
* If a [[logical disjunction|disjunction]] <math>X \lor Y</math><br/>{{spaces|4}}is true, then either <math>X</math> is true or <math>Y</math> is true;<br/>{{spaces|4}}is false, then <math>X</math>, <math>Y</math> are both false. 
* If a [[material conditional|conditional]] <math>X \to Y</math><br/>{{spaces|4}}is true, then either <math>X</math> is false or <math>Y</math> is true;<br/>{{spaces|4}}is false, then <math>X</math> is true and <math>Y</math> is false.
* If a [[negation]] <math>\neg X</math><br/>{{spaces|4}}is true, then <math>X</math> is false;<br/>{{spaces|4}}is false, then <math>X</math> is true.

The method of analytic tableaux is based on these facts. The main principle of propositional tableaux is to attempt to "break" complex formulae into smaller ones until complementary pairs of literals are produced or no further expansion is possible.

[[File:Prop-tableau-1.svg|thumb|100px|Initial tableau for {(a⋁¬b)⋀b,¬a}]]
The method works on a tree whose nodes are labeled with formulae. At each step, this tree is modified; in the propositional case, the only allowed changes are additions of a node as descendant of a leaf. The procedure starts by generating the tree made of a chain of all formulae in the set to prove unsatisfiability.<ref>A variant to this starting step is to begin with a single-node tree whose root is labeled by <math>\top</math>. In this second case, the procedure can always copy a formula in the set below a leaf. As a running example, the tableau for the set <math>\{(a \lor \neg b) \land b, \neg a\}</math> is shown.</ref> Then, the following procedure may be repeatedly applied nondeterministically:

# Pick an open leaf node. (The leaf node in the initial chain is marked open).
# Pick an applicable node on the branch above the selected node.<ref>An ''applicable'' node is a node whose outermost connective corresponds to an expansion rule, and which has not already been applied at any prior node on the selected leaf node's branch.</ref>
# Apply the applicable node, which corresponds to expanding the tree below the selected leaf node based on some expansion rule (detailed below).
# For every newly created node that is both a literal/negated literal, ''and'' whose complement appears in a prior node on the same branch, mark the branch as ''closed''. Mark all other newly created nodes as ''open''.

[[File:Prop-tableau-3.svg|thumb|180px|a⋁¬b generates a and ¬b]]
If a branch of the tableau contains a formula ...
* <math>\boldsymbol{\mathsf{T}}(X \land Y)</math>, add to its leaf the chain of two nodes containing the formulae <math>\boldsymbol{\mathsf{T}}(X)</math> and <math>\boldsymbol{\mathsf{T}}(Y)</math>;<ref>Read <math>\boldsymbol{\mathsf{T}}( \dots )</math> as "...is true"</ref>
* <math>\boldsymbol{\mathsf{F}}(X \land Y)</math>, create two sibling children to its leaf, containing the formulae <math>\boldsymbol{\mathsf{F}}(X)</math> and <math>\boldsymbol{\mathsf{F}}(Y)</math> respectively;<ref>Read <math>\boldsymbol{\mathsf{F}}( \dots )</math> as "...is false"</ref>
* <math>\boldsymbol{\mathsf{T}}(X \lor Y)</math>, create two sibling children to its leaf, containing the formulae <math>\boldsymbol{\mathsf{T}}(X)</math> and <math>\boldsymbol{\mathsf{T}}(Y)</math> respectively;
* <math>\boldsymbol{\mathsf{F}}(X \lor Y)</math>, add to its leaf the chain of two nodes containing the formulae <math>\boldsymbol{\mathsf{F}}(X)</math> and <math>\boldsymbol{\mathsf{F}}(Y)</math>;
* <math>\boldsymbol{\mathsf{T}}(X \to Y)</math>, create two sibling children to its leaf, containing the formulae <math>\boldsymbol{\mathsf{F}}(X)</math> and <math>\boldsymbol{\mathsf{T}}(Y)</math> respectively;
* <math>\boldsymbol{\mathsf{F}}(X \to Y)</math>, add to its leaf the chain of two nodes containing the formulae <math>\boldsymbol{\mathsf{T}}(X)</math> and <math>\boldsymbol{\mathsf{F}}(Y)</math>;
* <math>\boldsymbol{\mathsf{T}}(\neg X)</math>, add to its leaf the node containing the formula <math>\boldsymbol{\mathsf{F}}(X)</math>;
* <math>\boldsymbol{\mathsf{F}}(\neg X)</math>, add to its leaf the node containing the formula <math>\boldsymbol{\mathsf{T}}(X)</math>.

The breakdown process terminates after a finite number of steps, because each application of a rule eliminates a connective, and there are only finitely many connectives in any formula.


:{| style="border: 2px solid black; border-spacing: 30px; border-collapse: separate;"
<!-- |-
! colspan="4" style="text-align: center;" | Summary -->
|-
| style="vertical-align: top;" | <math>\frac{\boldsymbol{\mathsf{T}}(X \land Y)}{\begin{array}{c}\boldsymbol{\mathsf{T}}(X)\\\boldsymbol{\mathsf{T}}(Y)\end{array}}</math>
| style="vertical-align: top;" | <math>\frac{\boldsymbol{\mathsf{T}}(X \lor Y)}{\begin{array}{c}\boldsymbol{\mathsf{T}}(X) \mid \boldsymbol{\mathsf{T}}(Y)\end{array}}</math>
| style="vertical-align: top;" | <math>\frac{\boldsymbol{\mathsf{T}}(X \to Y)}{\begin{array}{c}\boldsymbol{\mathsf{F}}(X) \mid \boldsymbol{\mathsf{T}}(Y)\end{array}}</math>
| style="vertical-align: top;" | <math>\frac{\boldsymbol{\mathsf{T}}(\neg X)}{\begin{array}{c}\boldsymbol{\mathsf{F}}(X)\end{array}}</math>
|-
| style="vertical-align: top;" | <math>\frac{\boldsymbol{\mathsf{F}}(X \land Y)}{\begin{array}{c}\boldsymbol{\mathsf{F}}(X) \mid \boldsymbol{\mathsf{F}}(Y)\end{array}}</math>
| style="vertical-align: top;" | <math>\frac{\boldsymbol{\mathsf{F}}(X \lor Y)}{\begin{array}{c}\boldsymbol{\mathsf{F}}(X)\\\boldsymbol{\mathsf{F}}(Y)\end{array}}</math>
| style="vertical-align: top;" | <math>\frac{\boldsymbol{\mathsf{F}}(X \to Y)}{\begin{array}{c}\boldsymbol{\mathsf{T}}(X)\\\boldsymbol{\mathsf{F}}(Y)\end{array}}</math>
| style="vertical-align: top;" | <math>\frac{\boldsymbol{\mathsf{F}}(\neg X)}{\begin{array}{c}\boldsymbol{\mathsf{T}}(X)\end{array}}</math>
|}

'''Note''': In systems based on the grammar
:<math>\Phi ::= \bot \mid PV \mid (\Phi \to \Phi) \mid (\Phi \lor \Phi) \mid (\Phi \land \Phi)</math>,
that do not treat [[negation]] as primitive but define it in terms of implication and [[False (logic)#False, negation and contradiction|falsity]] (<math>\neg \Phi \, \overset{\text{def}}{=} \, \Phi \to \bot</math>),<br/>the tableau rules for <math>\neg</math> are replaced by

:{| <!-- style="border: 2px solid black; border-spacing: 10px; border-collapse: separate;" -->
|-
| style="vertical-align: top;" | <math>\boldsymbol{\mathsf{T}}(\bot)</math>
| :
| Close the branch (contradiction),
|-
| style="vertical-align: top;" | <math>\boldsymbol{\mathsf{F}}(\bot)</math>
| :
| Do nothing (since it just asserts no contradiction).
|}

The principle of tableau is that formulae in nodes of the same branch are considered in conjunction while the different branches are considered to be disjuncted. As a result, a tableau is a tree-like representation of a formula that is a disjunction of conjunctions. This formula is equivalent to the set to prove unsatisfiability. The procedure modifies the tableau in such a way that the formula represented by the resulting tableau is equivalent to the original one. One of these conjunctions may contain a pair of complementary literals, in which case that conjunction is proved to be unsatisfiable. If all conjunctions are proved unsatisfiable, the original set of formulae is unsatisfiable.