symbol The Skolem term is a constant (a function of arity 0) because the quantification over does not occur within the scope of any universal quantifier. If the original formula contained some universal quantifiers such that the quantification over was within their scope, these quantifiers have evidently been removed by the application of the rule for universal quantifiers. The rule for existential quantifiers introduces new constant symbols. These symbols can be used by the rule for universal quantifiers, so that can generate even if was not in the original formula but is a Skolem constant created by the rule for existential quantifiers. The above two rules for universal and existential quantifiers are correct, and so are the propositional rules: if a set of formulae generates a closed tableau, this set is unsatisfiable. Completeness can also be proved: if a set of formulae is unsatisfiable, there exists a closed tableau built from it by these rules. However, actually finding such a closed tableau requires a suitable policy of application of rules. Otherwise, an unsatisfiable set can generate an infinite-growing tableau. As an example, the set is unsatisfiable, but a closed tableau is never obtained if one unwisely keeps applying the rule for universal quantifiers to , generating for example . A closed tableau can always be found by ruling out this and similar "unfair" policies of application of tableau rules. The rule for universal quantifiers is the only non-deterministic rule, as it does not specify which term to instantiate with. Moreover, while the other rules need to be applied only once for each formula and each path the formula is in, this one may require multiple applications. Application of this rule can however be restricted by delaying the application of the rule until no other rule is applicable and by restricting the application of the rule to ground terms that already appear in the path of the tableau. The variant of tableaux with unification shown below aims at solving the problem of non-determinism. First-order tableau with unification The main problem of tableau without unification is how to choose a ground term for the universal quantifier rule. Indeed, every possible ground term can be used, but clearly most of them might be useless for closing the tableau. A solution to this problem is to "delay" the choice of the term to the time when the consequent of the rule allows closing at