# Semantic Tableau Algorithm

## Algorithm

Let $\mathbf A$ be a WFF of propositional logic.

The purpose of this algorithm is to create a completed semantic tableau $T$ for $\mathbf A$.

Step 1: Start with a labeled tree $T$ comprising only a root node labeled with the singleton $\left\{{\mathbf A}\right\}$.
Step 2: Choose a leaf node $t$ of $T$ that has not yet been marked. Let $U \left({t}\right)$ be the set that labels $t$.
Step 3: If $U \left({t}\right)$ is a set of literals, mark $t$ as follows:
a): If $U \left({t}\right)$ contains a complementary pair, mark it closed, $\times$, and go to Step 2.
b): Otherwise, mark it open, $\odot$, and go to Step 2.
Step 4: Choose a formula $\mathbf B \in U \left({t}\right)$ that is not a literal. Classify $\mathbf B$ as an $\alpha$-formula or a $\beta$-formula, and determine $\mathbf B_1, \mathbf B_2$ accordingly.
a): If $\mathbf B$ is an $\alpha$-formula, add a child $t'$ to $t$, labeled $U \left({t'}\right) = \left({U \left({t}\right) \setminus \left\{{\mathbf B}\right\}}\right) \cup \left\{{\mathbf B_1, \mathbf B_2}\right\}$.
b): If $\mathbf B$ is a $\beta$-formula, add two children $t', t''$ to $t$ with labels:
$U \left({t'}\right) = \left({U \left({t}\right) \setminus \left\{{\mathbf B}\right\}}\right) \cup \left\{{\mathbf B_1}\right\}$
$U \left({t''}\right) = \left({U \left({t}\right) \setminus \left\{{\mathbf B}\right\}}\right) \cup \left\{{\mathbf B_2}\right\}$
Step 5: Go to Step 2 if there remain leaves that are not marked. Otherwise, stop.

### Finiteness

The finiteness of this algorithm is demonstrated on Semantic Tableau Algorithm Terminates.

### Heuristics

The Semantic Tableau Algorithm can be made more efficient by using the following heuristic adaptations.

Firstly, the addition of a Step 2.5:

Step 2.5: If $U \left({t}\right)$ contains a complementary pair of formulas, mark $t$ closed and go to Step 2.

Secondly, the following modification to the initial part of Step 4:

Step 4: If possible, choose an $\alpha$-formula $\mathbf B \in U \left({t}\right)$; otherwise, choose a $\beta$-formula $\mathbf B$. Determine $\mathbf B_1, \mathbf B_2$ corresponding to $\mathbf B$ being an $\alpha$-formula or a $\beta$-formula.