Why is Prolog's failure by negation not considered logical negation?

Question

In many Prolog guides the following code is used to illustrate "negation by failure" in Prolog.

not(Goal) :- call(Goal), !, fail. 
not(Goal).

However, those same tutorials and texts warn that this is not "logical negation".

Question: What is the difference?

I have tried to read those texts further, but they don't elaborate on the difference.

Answer 1

I like @TesselatingHeckler's answer because it puts the finger on the heart of the matter. You might still be wondering, what that means for Prolog in more concrete terms. Consider a simple predicate definition:

p(something).

On ground terms, we get the expected answers to our queries:

?- p(something).
true.

?- \+ p(something).
false.

?- p(nothing).
false.

?- \+ p(nothing).
true.

The problems start, when variables and substitution come into play:

?- \+ p(X).
false.

p(X) is not always false because p(something) is true. So far so good. Let's use equality to express substitution and check if we can derive \+ p(nothing) that way:

?- X = nothing, \+ p(X).
X = nothing.

In logic, the order of goals does not matter. But when we want to derive a reordered version, it fails:

?- \+ p(X), X = nothing.
false.

The difference to X = nothing, \+ p(X) is that when we reach the negation there, we have already unified X such that Prolog tries to derive \+p(nothing) which we know is true. But in the other order the first goal is the more general \+ p(X) which we saw was false, letting the whole query fail.

This should certainly not happen - in the worst case we would expect non-termination but never failure instead of success.

As a consequence, we cannot rely on our logical interpretation of a clause anymore but have to take Prolog's execution strategy into account as soon as negation is involved.

Answer 2

• Logical claim: "There is a black swan".

• Prolog claim: "I found a black swan".

Finding a black swan is strong support for the claim that there is one.

• Logical negation: "There isn't a black swan".

• Prolog negation: "I have not found a black swan".

This is not strong support for the claim. "Did you even look? Did you look over there?". The logical version has no room for black swans anywhere, the Prolog version could have poor quality code, computing limits to searching the entire planet down to swan size areas, time limits for how long to spend searching before stopping; it leaves room for a black swan somewhere which the code didn't find. At worst there are black swans all around but a mistake in the code meant it didn't search anywhere.

The logical negation doesn't need anyone to look anywhere, the claim stands alone separate from any proof or disproof. The Prolog logic is tangled up in what Prolog can and cannot prove using the code you write.

Answer 3

There are a couple of reasons why,

Insufficient instantiation

A goal not(Goal_0) will fail, iff Goal0 succeeds at the point in time when this not/1 is executed. Thus, its meaning depends on the very instantiations that happen to be present when this goal is executed. Changing the order of goals may thus change the outcome of not/1. So conjunction is not commutative.

Sometimes this problem can be solved by reformulating the actual query.

Another way to prevent incorrect answers is to check if the goal is sufficiently instantiated, by checking that say ground(Goal_0) is true producing an instantiation error otherwise. The downside of this approach is that quite too often instantiation errors are produced and people do not like them.

And even another way is to delay the execution of Goal_0 appropriately. The techniques to improve the granularity of this approach are called constructive negation. You find quite some publications about it but they have not found their way into general Prolog libraries. One reason is that such programs are particularly hard to debug when many delayed goals are present.

Things get even worse when combining Prolog's negation with constraints. Think of X#>Y,Y#>X which does not have a solution but not/1 just sees its success (even if that success is conditional).

Semantic ambiguity

With general negation, Prolog's view that there exists exactly one minimal model no longer holds. This is not a problem as long as only stratified programs are considered. But there are many programs that are not stratified yet still correct, like a meta-interpreter that implements negation. In the general case there are several minimal models. Solving this goes far beyond Prolog.

When learning Prolog stick to the pure, monotonic part first. This part is much richer than many expect. And you need to master that part in any case.