Semantic Tableaux

A signed formula is an expression $A = b$ where $A$ is a formula and $b$ is a boolean value.

First, all occurrences of $\to$ and $\Leftrightarrow$ are replaced with their definitions so that the only connectives used are $\land$ and $\lor$ . Following this, AND-OR trees are used to analyse the formula.

We use branch expansion rules to create the tree:

(A_{1} \land \dots \land A_{n}) = 0 (A_{1} \land \dots \land A_{n}) = 1 (A_{1} \lor \dots \lor A_{n}) = 0 (A_{1} \lor \dots \lor A_{n}) = 1 (\neg A) = 0 (\neg A) = 1 ⇝ ⇝ ⇝ ⇝ ⇝ ⇝ A_{1} = 0 ∣ \dots ∣ A_{n} = 0 A_{1} = 1, \dots, A_{n} = 1 A_{1} = 0, \dots, A_{n} = 0 A_{1} = 1 ∣ \dots ∣ A_{n} = 1 A = 1 A = 0

A branch is closed if any of the following cases apply to it:

It contains both $p = 0$ and $p = 1$ for some atom $p$ .
It contains $⊤ = 0$ .
It contains $⊥ = 1$ .

If a branch remains open once all rules have been applied, then the formula is satisfiable. If all branches are closed, then the formula is unsatisfiable. A model can be extracted from a complete open branch by selecting signed atoms along the branch’s path.

A formula $A$ is valid if and only if there is a closed tableau for $A = 0$ . Formulae $A$ and $B$ are equivalent if and only if there is a closed tableau for $(A \leftrightarrow B) = 0)$ .

Warning

Demonstrating that there are no closed branches for $A = 1$ is not sufficient to show validity for $A$ .

CS Notes

Explorer

Semantic Tableaux

Graph View

Backlinks