# Definition:Semantic Tableau

## Definition

Semantic tableaus are the labeled trees which can be obtained in the course of executing the Semantic Tableau Algorithm.

### Semantic Tableau 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.

### Completed Tableau

Let $T$ be a semantic tableau.

Then $T$ is completed iff all of its leaves are marked.

### Closed Tableau

Let $T$ be a semantic tableau.

Then $T$ is closed iff all of its leaves are marked closed.

### Open Tableau

Let $T$ be a semantic tableau.

Then $T$ is open iff all of its leaves are marked open.