Pereira@SRI-AI@sri-unix.UUCP (08/23/83)
The predicate defined by
ugh(X) :- X, !, fail.
ugh(X).
( a.k.a. 'not' in some circles, a.k.a. \+ to DEC-20 Prolog/C-Prolog
users ) is NOT negation for two basic reasons:
1. The problem noted by Sanjai in the last Digest, which is well
known ( well, may be, well known in the Prolog underground... ).
Essentially, ugh (\+, not) should not be allowed to instantiate
variables in its argument.
2. Even if 1. didn't apply, it would still not be negation, but
rather "finite-failure non-provability", discussed in an excellent
theoretical paper by Lassez et al. at last week's IJCAI, and
previously analyzed by Apt and van Emden ( Journal of the ACM
vol. 29, no. 3, July 1982 ) and by Clark ( in Logic and Databases,
Gallaire and Minker eds., Plenum Press, NY, 1978 ).
Assuming we want negation as nonprovability in a certain context,
there is a conceptually simple cure to problem 1: delay \+ goals until
the goal is ground. If the goal never becomes ground, succeed printing
"solution if non-ground \+ goals"). As far as I know, this idea was
first suggested by Colmerauer and is implemented in Lee Naish's
MU-Prolog ( from Melbourne University ). There are efficiency problems
with his implementation, however, that have to do with the need to
scan the \+ goal over and over again to check it is fully ground
each time a variable in it is instantiated to some nonvariable term.
Given that DEC-20 Prolog and C-Prolog do not have the delaying
mechanism, Richard O'Keefe has implemented a version of \+ ( called
'not', sigh... ) that at least checks that all goals given to the
non-provability predicate are ground, and complains otherwise.
This helps spotting those illegitimate uses of non-provability.