Method of Analytic Tableaux - Searching For A Closed Tableau

Searching For A Closed Tableau

If a tableau calculus is complete, every unsatisfiable set of formula has an associated closed tableau. While this tableau can always be obtained by applying some of the rules of the calculus, the problem of which rules to apply for a given formula still remains. As a result, completeness does not automatically implies the existence of a feasible policy of application of rules that can always lead to building a closed tableau for every given unsatisfiable set of formulae. While a fair proof procedure is complete for ground tableau and tableau without unification, this is not the case for tableau with unification.

A general solution for this problem is that of searching the space of tableau until a closed one is found (if any exists, that is, the set is unsatisfiable). In this approach, one starts with an empty tableau and then recursively tries to apply every possible applicable rule. This procedure visits a (implicit) tree whose nodes are labeled with tableau, and such that the tableau in a node is obtained from the tableau in its parent by applying one of the valid rules.

Since one such branch can be infinite, this tree has to be visited breadth-first rather than depth-first. This requires a large amount of space, as the breadth of the tree can grow exponentially. A method that may visit some nodes more than once but works in polynomial space is to visit in a depth-first manner with iterative deepening: one first visits the tree up to a certain depth, then increases the depth and perform the visit again. This particular procedure uses the depth (which is also the number of tableau rules that have been applied) for deciding when to stop at each step. Various other parameters (such as the size of the tableau labeling a node) have been used instead.