10.2.7 Subsequent Instantiations: If we can't instantiate

Continuation.
We have just finished expanding the first recursive call of a conjunctive expansion (i.e. the expansion of the first conjunct). In this case we just pass through our complete quants-list to the second conjunct and let it care for the subsequent instantiations. Maybe the second conjunct will produce more individuals. This may allow us to re-instantiate some of the quantifiers that could not find any new individuals before.
Or we are at the leaf of an otherwise saturated branch. In this case we will recursively try to instantiate all quantifiers on quants as often as possible.

What do we have to do if the two base clauses explained before fail? In this case, we have reached an atomic formula, there is no clash and (more interestingly) we could not instantiate the first quantifier of our list. Hence we must be in one of two situations:

We have just finished expanding the first recursive call of a conjunctive expansion (i.e. the expansion of the first conjunct). In this case we just pass through our complete quants-list to the second conjunct and let it care for the subsequent instantiations. Maybe the second conjunct will produce more individuals. This may allow us to re-instantiate some of the quantifiers that could not find any new individuals before.
Or we are at the leaf of an otherwise saturated branch. In this case we will recursively try to instantiate all quantifiers on quants as often as possible.

Clause (c) handles the first of the discussed cases. It passes on the list of quantifiers:

% (c)

tabl(F,InBranch,[F|InBranch],Quants,Quants,_) :- !.

This leaves us with the second case: We're at a (current) leaf and want to work through the quantifiers that remain on our quants-list. Notice that we know that the first quantifier on the list can never be used again. Either it has used up its Qdepth or it has already been used with all the individuals there are. We know this because it's the reason why we got here - otherwise the heading quantifier would have been instantiated in the last call to clause (b).

Clause (d) thus throws away the now useless quantifier and starts a recursive call with the rest of our quants-list:

% (d)

tabl(F,InBranch,OutBranch,[_|RestQuants],QuantsOut,Qdepth) :- tabl(F,InBranch,OutBranch,RestQuants,QuantsOut,Qdepth).

10.000$ Question!

We have claimed that clause (d) applies if and only if its input formula F is at a current leaf of the tableaux. Now the 10.000$ question is: ``Why? How do we know when we're at a leaf, and how do we enforce that clause (d) is applied then?''. The answer to this is a little tricky. First of all, we have to ensure that clause (d) is applied at all. To do so, we instantiate QuantsOut with [] when we call our tabl/6-predicate at top-level. Otherwise, our program would always use clause (c) when it reaches a quantifier that it cannot instantiate in clause (b). The quantifier would ``block'' all others and our program would happily produce a full list of quantifiers on QuantsOut (headed by the ``blocking'' quantifier), most of which could probably still be instantiated. By requiring that QuantsOut (finally) be empty, we force our program to apply clause (d) to remove the ``blocking'' quantifier. In effect, we ensure that all quantifiers are instantiated as often as their Qdepth and the Herbrand base of the branch permit.

The answer

Now here is the central point of the answer to our question: If we reach a leaf (which is the last step in the construction of a branch), coindexing tells us that QuantsOut has to be the empty list - due to our top-level call. If there are quantifiers left on the QuantsIn list, we cannot enter the non-recursive clause (c) because the ...,Quants,Quants, ... in its head clashes. So we correctly choose clause (d).

So much for the``if''-direction in our claim that clause (d) is applied if and only if its input formula is at a current leaf. Now for the only if: The cut in clause (c) takes care of this. We will always choose clause (c) instead of clause (d) whenever we're not at a current leaf (i.e. we are expanding some ``first conjunct''). Clause (c) comes first in the program, and no constraints are put on the value of QuantsOut at inner nodes of a tableaux branch. Only at a leaf, the head of clause (c) won't match because we've set the empty list as QuantsOut at top-level. Now the cut in clause (c) ensures that none of our previous choices to enter (c) is backtracked on this clash and redone entering (d). In effect clause (d) can only be used to empty a quants list that has been built before, not to build another one instead.