p(X) as "there is no evidence for
p(X)" or "there is no proof for
References at the end of this page are of interest (as is the page):
Wikipedia: "Negation as Failure"
- Negation as failure (Keith Clark, 1878, 1987)
- Negation as Failure: A Comparison of Clark's Completed Data Dase and Reiter's Closed World Assumption J.C. Sheperdson, in: The Journal of Logic Programming, vol 1, 1984, pages 51–81.
- Negation as Failure II J.C. Sheperdson, in: The Journal of Logic Programming, vol 3, 1985, pages 185-202.
- Logic programming and negation: A survey, Krzysztof R. Apt, Roland N. Bol, in: The Journal of Logic Programming, Volumes 19–20, Supplement 1, May–July 1994, Pages 9-71
In Logic programming and negation: A survey, (Krzysztof R.Apt, Roland N.Bol, 1994), we read:
"One of the complications concerning SLDNF resolution is so-called floundering - a generation of a node which consists exclusively of nonground negative literals, because then selection of any literal ends the derivation in an abnormal way. In the definition here provided, floundering is treated differently - it arises as soon as a nonground negative literal is selected. Clearly, this small change has no effect on the theory of SLDNF resolution, since the original notion of floundering can be easily defined."
This seems to be about the following problem:
q(1). p(X) :- \+ q(X). % "Is it true that p(d)?" % Yes, because q(d) (ground) fails and thus \+ q(d) succeeds: "there is no proof of q(d)" ?- p(d). true. % "Is there any X such that p(X)?" % The correct answer would be "yes, any X different from 1" % which is not expressible in Prolog but _would_ be expressed by an enumeration if % the domain for P(X) were finite. % But the goal \+ q(X) with unbound X is "is there no X such that q(X)?" % An inconsistency arises! ?- p(X). false.
Maybe the Prolog processor should throw an exception when it finds a body subject to floundering.
The problem stems from the fact that Prolog basically relies on explicit enumerations over domains followed by tests (but for some reason, explicit domains have never been given explicit treatment in Prolog syntax and unification)
Explicitly specify the domain makes the problem go away because X is backtrackably ground:
?- member(X,[a,b,c]),p(X). X = a ; X = b ; X = c. ?- member(X,[1,2,3]),p(X). X = 2 ; X = 3.
If Prolog were more "modeling in logic" than "programming in logic" one could consider a symbolic answer describing the complement of
q(X) relative to the domain of p/1 as answer, something like a list comprehension:
?- p(X). setof(X,q(X),Xs), complement(Xs,domain(p/1),Result).
Using "double negation"
If you want to run some goal in an "isolated context":
\+ \+ Goal
The above really makes clear that you are only interested in whether Goal will succeed or fail and that any bindings shall be trashed and have no influence on further computation; (except for any side-effects generated when proving Goal, which are forever inscribed in the Universe and cannot be rolled back).
f(1,2). ?- A=2, ( \+ \+ f(X,A) ), format("X is now ~q\n", [X]). X is now _7808 A = 2.
Especially useful if you want to isolate your debugging printouts lest they change something due to small detail:
ddd_isolate(X) :- debug(topic,"X is ~q\n",[X]), (X= -> % ERROR: = instead of == debug(topic,"X is the empty list\n",) ; true). test(X) :- debug(topic), % switch on debug printing for topic "topic" debug(topic,"X before: ~q\n",[X]), \+ \+ ddd_isolate(X), debug(topic,"X after: ~q\n",[X]).
Yes, it works:
?- test(12). % X before: 12 % X is 12 % X after: 12 true. ?- test(). % X before:  % X is  % X is the empty list % X after:  true. ?- test(X). % X before: _5354 % X is _5354 % X is the empty list % X after: _5354 % changes have been erased true.