DEC-10 Prolog, C-Prolog, and Quintus Prolog all provide an "is-not-provable"
\+. The meaning of
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
) directly, so a clause of the form
p :- q, \+ r, s.
is compiled as if you had written
p :- q, ( r -> fail ; true ), s.
\+ 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.