not(
Goal)
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 database.
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 database, 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 that 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.