This chapter describes the predicates provided by library(not): not/1, '\='/2, '~='/2, and once/1. For comparison purposes, the negation facilities which are built into the Prolog system are also described.

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.

If the difference between the Prolog "is-not-provable" operator (\+) and the standard negation operator of logic is not taken into account, you may find that some of your programs will behave in an unexpected manner. Here is an example:

man(john). man(adam). woman(sue). woman(eve). married(adam, eve). married(X) :- married(X, _). married(X) :- married(_, X). human(X) :- man(X). human(X) :- woman(X).

The question

| ?-\+ married(Who).

is a perfectly good one, to which one might at first glance expect the response to be "john" or "sue". However, the meaning of this clause to Prolog is

is it the case that the term "married(Who)" has no provable instances?

to which the answer is "no", as "married(adam)" is an instance of "married(Who)" and is provable by Prolog. The question

| ?-\+ dead(X).

is also a perfectly good one, and after perhaps complaining that dead/1
is undefined, Prolog will report the answer "yes", because dead(X)
has no instance that can be proven from this data base. In effect, this
means "for all X, dead(X) is not provable". Even though "dead(adam)
is not provable" is a true consequence of this statement, Prolog will
__not__ report 'X = adam' as a solution of this question. This is not
the function of '`\+`'/1. Note also that "dead(adam) is false"
is __not__ a valid consequence of this data base, even though "dead(adam)
is not provable" is true. To deduce one from the other requires the
use of the "Closed World Assumption", which can be paraphrased
as "anything that I do not know and cannot deduce is not true".
See any good book on logic programming (such as *Foundations of Logic
Programming* by John Lloyd, Springer-Verlag 1984) for a fuller explanation
of this. We would very often like an operation which corresponds to logical
negation. That is, we would like to ask

| ?-not married(X).

and have Prolog tell us the names of some people who are not married, or to ask

| ?-not dead(X).

and have Prolog name some people who are not dead. The unprovability
operator will not do this for us. However, we __can__ use '`\+`'/1
as if it were negation, but only for certain tasks under some conditions
that are not very restrictive. The first condition is that if you want
to simulate not(p) with \+(p), you must first ensure that you have complete
information about p. That is, your program must be such that every true
ground instance of p can be proved in finite time, and that every false
ground instance of p will fail in finite time. Database programs often
have this property. Even then, given a non-ground instance of p, not(p)
would be expected to bind some of the variables of p. But by design, \+(p)
__never__ binds any variables of p. Therefore the second condition is
that when you call \+(p), p should be ground, or \+(p) will not simulate
not(p) properly. Checking the first condition requires an analysis of the
entire program. Checking that p is ground is relatively simple. Therefore,
the library file library(not) defines an operation

not Goal

which checks whether its Goal argument is ground, and if it is, attempts to prove "\+ Goal". Actually, the check done is somewhat subtler than that. The simulation can be sound even when some variables remain; for example, if left_in_stock(Part, Count) has at most one solution for any value of Part, then

\+ (left_in_stock(Part,Count), Count < 10)

is perfectly sound provided you do not use Count elsewhere in the clause.
You can tell not/1 that you take responsibility for a variable's being
safe by existentially quantifying it (see the description of `setof`/3),
so

not Count^(left_in_stock(Part,Count), Count < 10)

demands only that Part must be ground. Even so, this is not particularly good style, and you would be better off adding a predicate

fewer_in_stock_than(Part, Limit) :- left_in_stock(Part, Count), Count < Limit.

and asking the question

not fewer_in_stock_than(Part, 10)

If you want to find instances that do not satisfy a certain test, you can generally enumerate likely candidates and check each one. For example,

| ?-human(H), not married(H).H = john;H = sue | ?-man(M), not dead(M).M = john;M = adam

The present library definition of not/1 warns you when you would get the wrong answer, and offers you the choice of aborting the computation or accepting possible incorrect results.

DEC-10 Prolog, C-Prolog, and Quintus Prolog provide two inequality operations:

- Term1
`\==`Term2 - Term1 is not currently identical to Term2
- Expr1
`=\=`Expr2 - Expr1 and Expr2 are arithmetic expressions with different values

'`=\=`'/2 is reasonably straightforward. Either it is true, and
will remain true, or it is false, and will remain false, or the Prolog
system will report an error if it cannot determine which. Thus 1 `=\=`
2 is true, 1 `=\=` 1.0 is false, and _ `=\=` 3 will result
in an error message. '`\==`'/2 is not really a logical relation,
but a meta-logical relation like var/1. It tests whether two terms are
exactly identical, down to having the same variables in the same places.
It either succeeds or fails; and if it fails it will continue to do so,
but if it succeeds it may fail later on. For example,

| ?-X \== Y,% succeeds |X = Y,% succeeds, unifying X and Y |X \== Y.% FAILS, now that X and Y are unified no

It is safe to use '`==`'/2 and '`\==`'/2 to test the equality
of terms when you know in advance that the terms will be ground by the
time the test is made.

library(not) defines another inequality predicate, as do the C-Prolog and DEC-10 Prolog libraries:

- Term1 \= Term2
- Term1 and Term2 do not unify

This means exactly the same thing as

\+ Term1 = Term2

and is subject to the same problems as the use of unprovability to simulate
negation. However, when the terms are ground, it is more efficient than
'`\==`'/2.

Obviously, if we can have a version of '`\+`'/2 which checks
whether it is safe to proceed, we can have a version of '\='/2 which does
the same. So library(not) also defines a "sound inequality" predicate

- Term1 ~= Term2
- Term1 and Term2 are not equal

There are three cases: it may succeed, or fail, or warn you that there
is not enough information yet to tell. Note that '~='/2 is a bit more clever
than 'not(T1 `=` T2)' would be:

f(X, a) ~= f(Y, b)

will succeed (correctly) even though

not(f(X,a) = f(Y,b))

would complain about the unbound variables X and Y. As '~='/2 is sound and '\='/2 is not, we recommend that you use '~='/2 rather than '\='/2 in your Prolog code.

We have seen that

\+ Goal

and

( Goal -> false ; true )

have the same effect. The form

( Goal -> true ; false )

is also useful: it commits to the first solution of Goal. This operation has a name:

once Goal

once/1 is useful when you have a nondeterminate definition for Goal, but in this case you want to solve it determinately. For example, to find out if there are any married couples, you could use

once married(_, _)

If the predicate is really determinate in concept, it is better to make it determinate in definition as well, rather than to use once/1.

library(not) defines

not Goal Term1 \= Term2 Term1 ~= Term2 once(Goal)

The tests

\+ Goal Term1 \== Term2 Expr1 =\= Expr2

are built into Quintus Prolog already, and are described in the reference pages.

Copyright (C) 1997 AI International Ltd contact: product support sales information