Wolfgang Schwarz

Detecting Satisfiability with Free-Variable Tableaux

Recently I suggested the following restriction on free-variable tableaux:

The gamma rule must not be applied if the result of its previous application has not yet been replaced by the closure rule.

I think I've now found a proof that the restriction preserves completeness:

Let (GAMMA) be a gamma-node that has been expanded with a variable y even though the free variable x introduced by the previous expansion is still on the tree. I'll show that before the elimination of x, every branch that can be closed by some unifier U can also be closed by a unifier U' that does not contain y in any way (that is, y is neither in the domain nor in the range of the unification, nor does it occur as an argument of anything in the range of the unification.) Hence the expansion with y is completely useless before the elimination of x.

Before the y-expansion, no branch at any stage contains y. After the y-expansion, every open subbranch of (GAMMA) contains the formula created by the y-expansion, let's call it F(y). Among these branches select the one that first gets closed by some unifier U containing y in any way. Now I'll show that, whenever at some stage a formula G(y) containing y occurs on this branch, we can extend the branch by adding the same formula with every occurrence of y replaced by x.

At the stage immediately after the y-expansion, the only formula containing y is F(y). And because (GAMMA) has previously also been expanded with x, and x has not yet been eliminated, the branch also contains F(x). Next, assume that G(y) occurs at some later stage of the branch. Then it has been introduced either by application of an ordinary alpha-delta rule or by the closure rule. If it has been introduced by application of an alpha-delta rule then we can just as well derive G(x) from the corresponding ancestor with x instead of y (which exists by induction hypothesis). Now for the closure rule. Assume first this application of closure does not close the branch (but rather some other branch). Then by assumption, the applied unifier does not contain y in any way, Moreover, it does not replace x by anything else. So in particular, it will not introduce any new occurrences of y in any formula, and it will not replace any occurrences of x and y. Hence if G(y) is the result of applying this unifier to some formula G'(y), then G(x) is the result of applying the unifier to the corresponding formula G'(x).

Assume finally that the branch is now closed by application of some unifier U that contains y in any way. Let C1, -C2 be the unified complementory pair. (At least one of C1, C2 contains y, otherwise U wouldn't be minimal.) Then as we've just shown, the branch also contains the pair C1(y/x), -C2(y/x). Let U' be like U except that every occurrence of y (in its domain or range or in an argument of anything in its range) is replaced by x. Clearly, if U unifies C1 and C2, then U' unifies C1(y/x), C2(y/x).

In the other posting I also mentioned that this restriction can't detect the satisfiability of x((Fx y Fy) Gx), which the Herbrand restriction on standard tableaux can. (A simpler example is x((Fx Fa) Ga).) These cases can be dealt with by simply incorporating the Herbrand restriction into the Free Variable system:

Do not expand a gamma node if it has already been expanded more often than there are constants and function terms on the tree.

This restriction is justified by the fact that every closed free-variable tableau can easily be translated into a closed standard tableau: One only has to replace all function terms and variables introduced by the delta rule and the gamma rule, respectively, with (different) individual constants. And if a closed free-variable tableau violates the above restriction, then the translated standard tableau violates the Herbrand restriction. This means that at least one of the gamma-applications in the translated tableau was useless, and therefore also at least one of the gamma-applications in the original tableau.

(On a standard tableau with Herbrand restriction, at most one of the constants could have been introduced by application of the gamma rule itself. So if there are n different individual constants and function terms on the free-variable tableau, there can be at most n+1 different individual constants on the corresponding standard tree. This is why the above restriction is slightly weaker than the orginial Herbrand restriction: even if a gamma node has been expanded as often as there are constants and function terms on the tree, it may be expanded once again. (Alternatively, one could keep track of whether the first constant was introduced by a gamma rule.))