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 :-
          q,
          \+ r,
          s.
     

is compiled as if you had written

     p :-
          q,
          ( r -> fail ; true ),
          s.
     

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.