6.1.6 An Example - final Step

Let's now look at the final step of the computation, when the program finds the contradiction false(P) vs. true(P) and fails:

How did we get here?

How did we get here? In step (3), there are three goals on the stack: The top goal from step (2) has produced two new subgoals, which are now on top. The third goal is the one that was second in step (2). It remains untouched for the time being. Steps (4) and (5) merely consist of the obvious recursive calls triggered by the subgoals on the stack.

Literals

In steps (3) and (5), tabl/3 is called on a literal. Therefore these are the steps where output arguments get instantiated. We've indicated this by notating the corresponding assignments to the right of the stack at the respective nodes. In step (3) Out2 is instantited to [true(P)], and in step (5) Out1 gets determined to [false(Q),true(P)]. If there were no other goals on the stack in step (5) this would be the output of the whole computation.

Finding the Contradiction

But there still is the goal that was put on the stack in step (2) (corresponding to the rightmost conjunct in the original input formula). Finally, in step (6) this goal becomes top of the stack and is processed. The literal true(Q) is added to the incoming branch and a clash/1 test is performed (in the computation tree we've left out the clash/1-subgoals that come from tabl/3 calls on literals. You may have noticed this already at steps (3) and (5)). Because true(Q) contradicts false(Q) on the incoming branch, there is a clash and the computation fails.

In our example, there are no possibilities for doing anything else now. The fail means that Prolog answers no, all previous instantiations are undone and the variable for the outgoing model of our top level call (Out) remains undetermined. This reflects the fact that the tableaux for our input formula has only one branch, and that this one branch is closed, i.e. contains no model.

But next, we'll look at a case where there is an alternative branch that remains open. We'll have a branching computation tree there, and Prolog's fail will trigger backtracking.