The "is-not-provable" Operator

DEC-10 Prolog, C-Prolog, and Quintus Prolog all provide an "is-not-provable" operator \+. The meaning of

     \+ Goal

is that the Prolog system is unable to find any solution for Goal as it currently stands.

In operational terms, we have

     \+ Goal :-
         ( call(Goal) -> fail
         ; true

In DEC-10 Prolog and C-Prolog, this is exactly how \+ is implemented. In Quintus Prolog there is a slight difference: the Quintus Prolog compiler supports (if -> then ; else) directly, so a clause of the form

     p :-
          \+ r,

is compiled as if you had written

     p :-
          ( r -> fail ; true ),

If \+ were not known to the compiler, the form r would be built as a data structure and passed to \+ to interpret, which would be slower and would require more memory. The extra efficiency of having \+ handled directly by the compiler is well worth having.