Semantic Tableau Algorithm/Heuristics

Algorithm

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.

Also see

• Correctness of Heuristics for Semantic Tableau Algorithm

Sources

• 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.) ... (previous) ... (next): $\S 2.6.4$