8.1.1 Literals

The first clause of the main tableaux predicate.

The recursive predicate tabl/3 implements the core of our tableaux system.

The first argument of tabl/3 is the input formula. In the first call, this is the formula with which we start our tableaux. The second argument (InBranch) stores the literals we have derived so far on the branch under construction. In the first call this argument will just be the empty list [], but we need it as an accumulator in the recursion.

The last argument (OutBranch) of tabl/3 will finally contain the model we've constructed on some branch (as a list of literals). In Chapter 9 we will learn how to use tableaux for a task called model generation. In this setting, OutBranch will be the output of our predicate. But for the time being, you can safely ignore this argument except when we mention it explicitely.

The predicate tabl/3 has six clauses. The base case is for literals, whereas the recusrive clauses handle complex formulae. We will first look at the base case. It is the last clause in the program, after the clauses for the complex formulae, so we can be sure that its input F is a literal. (Of course to be sure of this, we additionally have to include cuts in the other clauses to prevent backtracking to the ``literal case''). Here it is:

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

In this clause, we determine whether F is compatible with our input model. We add F to InBranch, then test if it was compatible. If it was, we return the result (in OutBranch). Otherwise the clause fails. Remember that InBranch contains all the literals that we have already derived on the current branch. If the new literal we're considering contradicts any of these facts, the current branch is closed. So in effect we signal branch closure by letting the above clause of tabl/3 fail.

The compatibility check we do is actually a negated incompatibility check. It is done by calling the auxiliary predicate clash/1 on OutBranch (which is equivalent to InBranch together with the new literal F).

The predicate clash/1 is implemented as follows:

clash(List) :-  
        member(true(A),List),
        member(false(A),List).

In our implementation we simply translate the signs of our calculus () into the Prolog atoms true respectively false. Our predicate clash/1 looks whether the list Literals contains the same atomic formula A twice, once signed true and once signed false.

?- Question!

A simpler clash test would suffice for our purposes (and make the program more efficient). Do you have an idea how to implement one?


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