prologlogicnegationnegation-as-failure

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


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.


Solution

  • 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.