Semantic Tableau Algorithm

From ProofWiki
Jump to navigation Jump to search

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