Editing Method of analytic tableaux (section)

===First-order tableau without unification===

A first-order formula <math>\forall x . \gamma(x)</math> implies all formulae <math>\gamma(t)</math> where <math>t</math> is a [[ground term]]. The following inference rule is therefore correct:

:<math>(\forall) \frac{\forall x . \gamma(x)}{\gamma(t)}</math> where <math>t</math> is an arbitrary ground term

Contrarily to the rules for the propositional connectives, multiple applications of this rule to the same formula may be necessary. As an example, the set <math>\{\neg P(a) \lor \neg P(b), \forall x . P(x)\}</math> can only be proved unsatisfiable if both <math>P(a)</math> and <math>P(b)</math> are generated from <math>\forall x . P(x)</math>.

Existential quantifiers are dealt with by means of Skolemization. In particular, a formula with a leading existential quantifier like <math>\exists x . \delta(x)</math> generates its Skolemization <math>\delta(c)</math>, where <math>c</math> is a new constant symbol.

:<math>(\exists) \frac{\exists x . \delta(x)}{\delta(c)}</math> where <math>c</math> is a new constant symbol

[[File:First-order tableau.svg|thumb|350px|A tableau without unification for {∀x.P(x),&nbsp;∃x.(¬P(x)⋁¬P(f(x)))}. For clarity, formulae are numbered on the left and the formula and rule used at each step is on the right.]]
The Skolem term <math>c</math> is a constant (a function of [[arity]] 0) because the quantification over <math>x</math> does not occur within the scope of any universal quantifier. If the original formula contained some universal quantifiers such that the quantification over <math>x</math> 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 <math>\forall y . \gamma(y)</math> can generate <math>\gamma(c)</math> even if <math>c</math> 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 <math>\{\neg P(f(c)), \forall x . P(x)\}</math> is unsatisfiable, but a closed tableau is never obtained if one unwisely keeps applying the rule for universal quantifiers to <math>\forall x . P(x)</math>, generating for example <math>P(c), P(f(c)), P(f(f(c))), \ldots</math>. 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 <math>(\forall)</math> 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.