10.2.6 Subsequent Instantiations: Instantiate

Continuation

Fairness

The rest of our four clauses together manage the successive fair instantiation of the quantifiers collected on the quants-list. In short, our strategy is to always make one instantiation of one quantifier every time we raech an atomic formula. Then we continue our tableaux with the instantiated scope. The next time we derive an atomic formula, we shift to the next quantifier, instantiate it, go on with the instance etc. If we shift past the end of our quants, we start again at the beginning. Rotating like this, we ensure fairness - every member of quants will get its share.

Enforcing termination

As far as described, our strategy would keep on rotating and instantiating the quants indefinitely. Of course we have to control this somehow. This is where the Qdepth argument comes in: We instantiate each quantifier at most Qdepth-times. Additionally, as we argued above, we will only make instantiations if they contribute something new.

The second base clause does all this. It takes a quantifier from the quants list, checks the side conditions just discussed, and eventually generates a new instance. Plus - after all it's a clause for literals - it extends the branch we're on by its input literal.

% (b)

tabl(F,InBranch,OutBranch,[(forall(X,Scope),SoFarInds)|RestQuants],QuantsOut,Qdepth) :-
        length(SoFarInds,LengthInds),
        LengthInds =< Qdepth,
        hbaseList([F|InBranch],HBase),
        member(Ind,HBase),
        \+ member(Ind,SoFarInds),!,
        subst([X:Ind],Scope,NewInstantiation),
        append(RestQuants,[(forall(X,Scope),[Ind|SoFarInds])],NewQuants),
        tabl(true(NewInstantiation),[F|InBranch],OutBranch,NewQuants,QuantsOut,Qdepth).

Let us go through the code in more detail. First, we use Prolog arithmetics to check if the given Qdepth is not exceeded. Second, with the help of member checks, we look for an individual that has not been used with the quantifier yet (i.e. we check if any instantiation would contribute anything new). If there is one, we take it (and the cut commits us to stick to the clause we are in). We then generate the new instantiation with our individual as explained earlier.

Finally, there is the recursive call with our new formula (the instantiated scope), where we have added the input literal F to our model. We know that there is no clash with that formula so far, because otherwise clause (a) would have applied. Note that we append the quantifier tuple we have considered to the back of the quants-list. This is how we implement ``rotating'' the quants-list.

The clause we've seen will fail once it arrives at a quantifier that has either used up it's full Qdepth or that has already been instantiated with all the individuals currently known. Next, we will see what happens in clauses (c) and (d), which handle these cases.

What are all the cuts for?

But before we go on, let us comment some more on the cuts in the clauses we're looking at: Note that we make double use of Prolog failure. On the one hand the explicit fail in clause (a) means as much as ``This branch is closed''. Backtracking should in this case directly lead to the next branch of the tableaux. But on the other hand we also use failure and backtracking to navigate between the three clauses (b), (c) and (d). As we shall see, one of these clauses will always succeed. The cut in clause (a) expresses the ``difference in meaning'' between these two uses of fail.

We are right now talking about what happens if we do not reach the cut clause (a), that is if our branch is not closed and we must backtrack to clauses (b)-(d). As we have seen above, clause (b) generates new instantiations of the first universial quantifier on the quants list if possible. Next we will see what clauses (c) and (d) do in case clause (b) fails.


Aljoscha Burchardt, Stephan Walter, Alexander Koller, Michael Kohlhase, Patrick Blackburn and Johan Bos
Version 1.2.5 (20030212)