Tableaux

logic propositional-logic

Definition

Semantic Tableau

The semantic tableau is a decision procedure for checking satisfiability of propositional formulas. It works by systematically decomposing a formula into simpler components using inference rules applied to signed formulas of the form $t:A$ (true) and $f:A$ (false).

If all branches close, the formula is unsatisfiable. If any open branch remains, it provides a model.

Properties

Soundness

Soundness

If the tableau closes, the formula is unsatisfiable.

Completeness

Completeness

If the formula is unsatisfiable, the tableau will close (given systematic rule application).

Complexity

Complexity

For a formula of size $n$, the tableau can have at most $O(n)$ distinct subformulas on any branch. In the worst case, the tableau may have $O(2^n)$ branches, but formula structure often leads to much smaller tableaux.

Branches

Open Branch

Definition

Open Branch

A branch in a semantic tableau is open when it is complete, meaning no further rules can be applied, and it contains no pair $t:A$ and $f:A$ for the same formula $A$.

An open branch certifies that the initial formula is satisfiable.

Link to original

Closed Branch

Definition

Closed Branch

A branch in a semantic tableau is closed when it contains both $t:A$ and $f:A$ for some formula $A$. This represents a contradiction: the same formula cannot be both true and false under one interpretation.

A tableau is closed when all of its branches are closed.

Link to original

Inference Rules

The tableau rules decompose signed formulas based on their main connective. Each rule specifies how to extend the tableau when a formula of a given form appears.

Conjunction

Definition

Conjunction

$$\frac{t:(A\wedge B)}{t:At:B}\frac{f:(A\wedge B)}{f:A\mid f:B}$$

The $t$-rule for $\wedge$ creates a single branch (both conjuncts must hold). The $f$-rule creates two branches (at least one conjunct must fail).

Link to original

Disjunction

Definition

Disjunction

$$\frac{t:(A\vee B)}{t:A\mid t:B}\frac{f:(A\vee B)}{f:Af:B}$$

Link to original

Negation

Definition

Negation

$$\frac{t:(\neg A)}{f:A}\frac{f:(\neg A)}{t:A}$$

Link to original

Implication

Definition

Implication

$$\frac{t:(A\to B)}{f:A\mid t:B}\frac{f:(A\to B)}{t:Af:B}$$

Link to original

Equivalence

Definition

Equivalence

$$\frac{t:(A\leftrightarrow B)}{\begin{array}{c}t:At:B\\ \mid \\ f:Af:B\end{array}}\frac{f:(A\leftrightarrow B)}{\begin{array}{c}t:Af:B\\ \mid \\ f:At:B\end{array}}$$

Link to original

Construction

Building a Tableau

To check whether a formula $A$ is satisfiable:

1. Start with $t:A$ as the root
2. Repeatedly apply tableau rules to unprocessed signed formulas
3. A branch closes if it contains both $t:B$ and $f:B$ for some formula $B$
4. The tableau is closed if all branches close
5. If any open branch remains after all rules are applied, the formula is satisfiable

An open branch gives a satisfying assignment: assign $\top$ to every atom $p$ where $t:p$ appears, and $\perp$ to every atom $p$ where $f:p$ appears.

Connection to Splitting

Relation to Splitting

The tableau method is closely related to the splitting algorithm. Both perform case analysis on formulas, but tableaux work directly with the formula structure rather than substituting truth values. The splitting tree and tableau tree for the same formula have essentially the same structure.

Comparison with Other Methods

Method	Works on	Key operation
Truth tables	All variables	Enumerate $2^n$ assignments
Splitting	Formula with substitutions	Case analysis on atoms
Tableaux	Signed formulas	Decomposition rules
DPLL	Clause sets	Unit propagation + splitting
Resolution	Clause sets	Resolving complementary literals

Examples

$t:\neg A$ and $t:(A\to B)$

Start with the branch

$$t:\neg A,t:(A\to B).$$

Apply the negation rule to $t:\neg A$:

$$f:A.$$

Apply the implication rule to $t:(A\to B)$:

$$\frac{t:(A\to B)}{f:A\mid t:B}.$$

This gives two branches:

$$f:A\mid f:A,t:B.$$

The tableau tree is:

Neither branch contains both $t:C$ and $f:C$ for the same formula $C$. Hence no branch closes, so there is no closed tableau derivation.

A model is given by $A=\perp$.

$f:A$ and $t:(A\to B)$

Start with the branch

$$f:A,t:(A\to B).$$

Apply the implication rule to $t:(A\to B)$:

$$\frac{t:(A\to B)}{f:A\mid t:B}.$$

This gives two branches:

$$f:A\mid f:A,t:B.$$

The tableau tree is:

The left branch only repeats $f:A$. The right branch contains $f:A$ and $t:B$, which are not contradictory. Hence at least one open branch remains, so there is no closed tableau derivation.

A model is given by $A=\perp$.

$t:\neg B$ and $t:(A\vee B)$

Start with the branch

$$t:\neg B,t:(A\vee B).$$

Apply the negation rule to $t:\neg B$:

$$f:B.$$

Apply the disjunction rule to $t:(A\vee B)$:

$$\frac{t:(A\vee B)}{t:A\mid t:B}.$$

This gives two branches:

$$f:B,t:A\mid f:B,t:B.$$

The tableau tree is:

The right branch closes because it contains both $f:B$ and $t:B$. The left branch remains open because $f:B$ and $t:A$ are compatible. Therefore the tableau is not closed, so there is no closed tableau derivation.

A model is given by $A=\top$ and $B=\perp$.

$f:A$ and $t:(A\wedge B)$

Start with the branch

$$f:A,t:(A\wedge B).$$

Apply the conjunction rule to $t:(A\wedge B)$:

$$\frac{t:(A\wedge B)}{t:At:B}.$$

This gives the single branch

$$f:A,t:A,t:B.$$

The tableau tree is:

The branch closes because it contains both $f:A$ and $t:A$. Since this is the only branch, the whole tableau is closed. Hence there is a closed tableau derivation.

Modus Ponens Validity

Check whether $(p\to q)\wedge p\to q$ is valid by testing whether its negation is unsatisfiable.

Step 1: Start with the negation.

Step 2: Apply negation rule ($t$).

Step 3: Apply implication rule ($f$). Creates two subgoals on the same branch.

Step 4: Apply conjunction rule ($t$). Adds both conjuncts to the branch.

Step 5: Apply implication rule ($t$) to $t:(p\to q)$. Creates two branches.

Step 6: Both branches close.

Both branches close, so the negation is unsatisfiable. Therefore $(p\to q)\wedge p\to q$ is valid.