8.1.2 Complex Formulae: Negation
The clause of the main tableaux predicate for negation.
We now have dealt with the literal case. But we still have to deal with complex formulae. Let us start with the clauses for negation, directly modeled on the rule 
.
tabl(true(~A),InBranch,H) :-
!,tabl(false(A),InBranch,H).
tabl(false(~A),InBranch,H) :-
!,tabl(true(A),InBranch,H).These clauses are almost self-explaining. They simply strip off the negation symbol and turn the sign of the formula. The cuts are there to prevent backtracking to the clause for literals, which would also match.
The recursive call covers the branch of the tableaux below the negated formula. Generally, all clauses for complex formulae will consist of recursive calls to tabl/3 on the decomposed input. Failure in one of these calls always means that the corresponding part of the tableaux is closed. In Section 8.1.5 we illustrate all this by an example.