Semantic Tableau Algorithm/Heuristics

From ProofWiki
Jump to: navigation, search


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.

Also see