Editing Method of analytic tableaux (section)

==Searching for a closed tableau==

If a tableau calculus is complete, every unsatisfiable set of formulae 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 imply the existence of a feasible policy of application of rules that always leads to 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.

[[File:Search tree of tableau space.svg|thumb|700px|A search tree in the space of tableaux for {∀x.P(x),&nbsp;¬P(c)⋁¬Q(c),&nbsp;∃y.Q(c)}. For simplicity, the formulae of the set have been omitted from all tableau in the figure and a rectangle used in their place. A closed tableau is in the bold box; the other branches could be still expanded.]]
A general solution for this problem is that of searching the space of tableaux 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 applies every possible applicable rule. This procedure visits a (implicit) tree whose nodes are labeled with tableaux, and such that the tableau in a node is obtained from the tableau in its parent by applying one of the valid rules.

Since each 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 depth first 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.

===Reducing search===

The size of the search tree depends on the number of (children) tableaux that can be generated from a given (parent) one. Reducing the number of such tableaux therefore reduces the required search.

A way for reducing this number is to disallow the generation of some tableaux based on their internal structure. An example is the condition of regularity: if a branch contains a literal, using an expansion rule that generates the same literal is useless because the branch containing two copies of the literals would have the same set of formulae of the original one. This expansion can be disallowed because if a closed tableau exists, it can be found without it. This restriction is structural because it can be checked by looking at the structure of the tableau to expand only.
 
Different methods for reducing search disallow the generation of some tableaux on the ground that a closed tableau can still be found by expanding the other ones. These restrictions are called global. As an example of a global restriction, one may employ a rule that specifies which of the open branches is to be expanded. As a result, if a tableau has for example two non-closed branches, the rule specifies which one is to be expanded, disallowing the expansion of the second one. This restriction reduces the search space because one possible choice is now forbidden; completeness is however not harmed, as the second branch will still be expanded if the first one is eventually closed. As an example, a tableau with root <math>\neg a \land \neg b</math>, child <math>a \lor b</math>, and two leaves <math>a</math> and <math>b</math> can be closed in two ways: applying <math>(\land)</math> first to <math>a</math> and then to <math>b</math>, or vice versa. There is clearly no need to follow both possibilities; one may consider only the case in which <math>(\land)</math> is first applied to <math>a</math> and disregard the case in which it is first applied to <math>b</math>. This is a global restriction because what allows neglecting this second expansion is the presence of the other tableau, where expansion is applied to <math>a</math> first and <math>b</math> afterwards.