This would work if clause/2 always failed if there is no matching clause. Indeed, in some systems, that was the case. But now, clause/2 may and will throw an er

This would work if clause/2 always failed if there is no matching clause. Indeed, in some systems, that was the case. But now, clause/2 may and will throw an error for example on: ?- clause(true, B). ERROR: No permission to access private_procedure `true/0' See also the Prolog ISO standard: clause(+head, ?callable_term) 8.8.1.3 Errors ... c) The predicate indicator Pred of Head is that of a private procedure - permission_error(access, private_procedure, Pred). ... In this interpreter, the third clause of prove/2 is also applicable if the others are applicable, because L1 subsumes both true and terms of the form (X,Y). For this reason, we get for example: ?- prove((true,true), _), false. ERROR: No permission to access private_procedure `true/0' whereas we expect this to succeed, because (true,true) does. Hence, to make this interpreter actually work, more must be added, and to make it meta-circular (i.e., able to interpret its own code), these features must then also be handled. In the representation I used, these issues do not arise because I am using a so-called clean representation. With such a representation, I can tell for certain what the individual goals are, as the individual goals are symbolically distinguished from conjunctions of goals.