Definition:Semantic Tableau

From ProofWiki
Jump to navigation Jump to search

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 if and only if all of its leaves are marked.


Closed Tableau

Let $T$ be a semantic tableau.


Then $T$ is closed if and only if all of its leaves are marked closed.


Open Tableau

Let $T$ be a semantic tableau.


Then $T$ is open if and only if all of its leaves are marked open.


Sources