Negation as Failure

Analogy categoryAnalogies

\+ Goal succeeds if Goal cannot be proven true from the current database, and fails if Goal can be proven. This is negation as failure, not classical logical negation: Prolog doesn't establish that Goal is actually false, only that it could not find a proof for it given what the database currently contains.

🏏

Cricket analogy: Ruling a batter 'not out' simply because the fielding side couldn't produce clear evidence of a catch is negation as failure -- the umpire doesn't prove innocence, only notes the absence of proof of guilt, exactly how \+ Goal succeeds when Goal can't be proven.

The Closed-World Assumption

Negation as failure rests on the closed-world assumption: Prolog treats its database as a complete description of what's true, so anything it cannot prove is treated as false. The classic pattern bird(X) :- \+ abnormal(X) implements default reasoning this way, assuming a bird flies unless an exception fact records it as abnormal -- and it depends entirely on the database actually containing every relevant exception.

🏏

Cricket analogy: A team assumes a player is fit to play unless the injury list explicitly says otherwise -- anything not listed as injured is treated as available, the same closed-world assumption Prolog makes: whatever isn't provably true is treated as false.

prolog

bird(tweety).
bird(polly).
bird(pingu).

penguin(pingu).

abnormal(X) :- penguin(X).

flies(X) :-
    bird(X),
    \+ abnormal(X).

?- flies(tweety).
true.

?- flies(pingu).
false.

Negation and Unbound Variables

Calling \+ Goal when Goal contains unbound variables that need to range over many possible values is unsafe: the negation cannot meaningfully check a well-defined condition and can flounder, producing results that don't correspond to a sound logical statement. The standard advice is to fully instantiate the arguments Goal depends on before negating it.

🏏

Cricket analogy: Asking 'is there any batter who is not out?' without specifying which batter is like calling \+ Goal on an unbound variable -- Prolog can't meaningfully search a whole open field of possibilities and the negation gives an unreliable or premature answer.

Negation vs the Cut-Fail Combo

Internally, \+ Goal is typically defined as call(Goal), !, fail ; true: if Goal succeeds even once, the cut commits and fail forces the negation itself to fail; if Goal never succeeds, the else branch makes the negation succeed. This means \+ Goal only checks whether Goal has at least one proof and then stops -- it never backtracks to explore Goal's other possible solutions.

🏏

Cricket analogy: Once the third umpire fails to find any angle proving a catch clean, that ruling is final for the delivery -- there's no retrying with a different camera after the decision is locked in, mirroring how \+ Goal commits to failure via cut once Goal's proof attempt fails, without revisiting Goal's other possible solutions.

Because \+ Goal is effectively call(Goal), !, fail ; true under the hood, it inherits cut's commit-and-stop behavior: it only checks whether Goal has at least one proof, then stops -- it never enumerates Goal's alternative solutions the way a normal call would. This also means \+ Goal called with unbound variables can flounder, silently proving the wrong thing (for instance \+ member(X, [1,2,3]) can succeed by binding X to some value outside the list rather than meaningfully asking 'is there no such X'). Always instantiate Goal's relevant arguments before negating it.

\+ Goal succeeds if Goal cannot be proven true from the current database, and fails if Goal can be proven.
This is negation as failure, not classical logical negation -- it reflects the closed-world assumption that anything not provable is treated as false.
The classic bird(X):- \+ abnormal(X) pattern implements default reasoning: assume normal behavior unless an exception is recorded.
Negation as failure can give incorrect results if the database is incomplete, since absence of proof isn't true logical falsity.
Calling \+ Goal with unbound variables in Goal is unsafe and can flounder or return misleading results.
Internally, \+ Goal is defined using cut and fail (call(Goal), !, fail ; true), so it commits after the first proof attempt rather than exploring Goal's alternatives.
Best practice is to fully instantiate the arguments of Goal before negating it with \+.