10.2.5 Universal Rule: Subsequent Instantiations

Continuation

In the previous section, we have seen how we store a universal quantifier. What remains to be discussed is how to re-use the quantifiers from our quants-list. This happens in the base case of tabl/6 (whenever we arrive at a literal). Before we look at the details, let us consider again the corresponding part of the implementation for PLNQ.

One propositional base clause

In the implementation of PLNQ we have the following (base) clause for literals:

tabl(F,InBranch,OutBranch) :-  
        OutBranch = [F|InBranch],
        \+ clash(OutBranch).

Reaching this clause, the only thing to do is to add the new literal to the current model. If there is a contradiction, the predicate fails and we know we are on a closed branch. Otherwise we are...

  1. ...either inside some tableau branch (if this was the last step of the first call of a conjunctive expansion). In this case, the second call takes over, or we are...

  2. ... at the leaf of a saturated branch. In this case, we are done with this branch.

Four first-order base clauses

In the case of first-order expansions, the situation is different. If we reach an atomic formula, there may be quantifiers on our list that still can (and must) be applied. This gives us some choices. Therefore we now have four clauses ((a)-(d)) instead of our former single base clause. The first clause is harmless - it is almost identical to the base clause of our old implementation and does not have to care about quantifiers at all. It looks for a contradiction on our branch including the new literal. If it it finds one, it signals this using fail, and we know that the branch is closed (like in the old implementation).

foTabl.pl: View Download

% (a)

tabl(F,InBranch,OutBranch,_,_,_) :-  
        OutBranch = [F|InBranch],
        clash(OutBranch),!,fail.

We do not want to (in fact we mustn't) consider any of the other clauses of our extended base case once we have found a clash. Hence the cut immediately after the clash test. But if the clash/1-test itself fails, we are not yet behind the cut. We can (and must) thus try the next clauses.


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