6.1.5 An Example - first Steps

Here comes an example that will help us understand how the clauses of tabl/3 are related to the construction of a tableaux as we would usually draw it. Let's take the formula , and suppose we want to make it false. This should result in a closed one-branch tableaux, containing the contradiction vs. . Now let's see how our program finds this tableaux.

Computation Tree

We represent Prolog's computation using a so called computation tree . This tree shows the sequence of calls that Prolog has to execute in order to prove its main goal (the one given in the initial call). Each node of a computation tree corresponds to a state of the computation. Each node contains a stack with the goals that have to be proven at the corresponding state of the computation. The topmost goal on the stack is always the one just under consideration at that state. If this goal produces new subgoals, they replace it on top of the stack in the next state (i.e. at the daughter node in the computation tree). If a goal succeeds, it is removed, but the resulting instantiations of variables are kept and used for the goals on the stacks below in the tree, which are still to be processed.

Computation trees branch whenever there are multiple clauses compatible with a call (i.e. in the case of a disjunction in the Prolog code). The branchings correspond to backtracking points in the programm. The computation tree for our running example does not branch, but we will soon see one that does.

Initial State

We start with an initial tableaux consisting of our input formula only, and a computation tree with only one node that contains the top goal:

Steps One and Two

In the following step, the negation symbol is stripped off and the sign of the whole formula is turned from to . We don't show the tableaux and computation tree for this step. We directly look at the next one, where the conjunction is handled. From now on, we will abbreviate as and as . The dotted boxes on the tableaux indicate how the formulae on the tableaux derive from each other: All formulae within a box (transitively) derive from the topmost one in that box. So the tree and tableaux after handling the first conjunction look as follows:

Notice that now for the first time, the stack in our computation tree contains two goals. This is because we had to handle a conjunction in step (1) and the clause of tabl/3 for conjunction consists of two subgoals, namely the two recursive calls to tabl/3 on the two conjuncts. The call for the first conjunct is top - Prolog will first consider this goal.

Looking at the Tableaux

But what does this mean on the side of the tableaux? It means that the tableaux will (for some time) grow "in the middle": below the formula we've added for the first conjunct (the blue one), but above the one for the second conjunct. Thus the next formulas are added inside the dotted box around the first conjunct.