# Semantic Tableau Algorithm

Jump to navigation
Jump to search

## Contents

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

## Sources

- 2012: M. Ben-Ari:
*Mathematical Logic for Computer Science*(3rd ed.) ... (previous) ... (next): $\S 2.6.2$: Algorithm $2.64$