Semantic Tableau Algorithm/Heuristics
Jump to navigation
Jump to search
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
Sources
- 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.) ... (previous) ... (next): $\S 2.6.4$