8.1.3 Complex Formulae: Conjunctive Expansion
The clause of the main tableaux predicate for conjunctive expansion.
We now look at the clause for positive conjunction, which corresponds to the rule 
. Again, the cut prevents backtracking to the clause for literals.
tabl(true(A & B),InBranch,OutBranch) :-
!,tabl(true(A),InBranch,K),
tabl(true(B),K,OutBranch). To make a conjunction true, we first make the first conjunct true. Then we take what model we've generated for the first conjunct (contained in K) and use it as input to make the second conjunct true. Note that here we really need the last argument of tabl/3.
If the second call to tabl/3 succeeds in the end, OutBranch contains all the literals generated when verifying both the first and second conjunct.
This is related to the way we would normally (with pen and paper) construct a tableaux as follows: Each one of the two recursive calls to tabl/3 in this clause covers one part of the branch below the conjunctive formula. If any of these two calls fails, so will the whole clause containing them. This is correct because both calls cover part of the same branch, and closure in any of these parts should affect the branch as a whole.