Semantic Tableau Algorithm
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.
This article is complete as far as it goes, but it could do with expansion. You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding this information. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Expand}} from the code.If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page. |
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 $\map U t$ 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 \map U t$; 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$