Negation as failure is the term used to describe how
we use the closed world assumption to implement a
form of
negation in Prolog. We now give an example which uses a rule
to define women in terms of them not being men. Logically,
x 
people ( 
man(x) 
woman(x)).
man(jim).The strategy is: to solve the goal woman(jim) try solving man(jim). This succeeds ---therefore woman(jim) fails. Similarly, woman(jane) succeeds. But there is a problem. Consider:man(fred).
woman(X):-
\+( man(X) ).?- woman(jim).
no
?- woman(X).It succeeds if man(X) fails ---but man(X) succeeds with X bound to jim. So woman(X) fails and, because it fails, X cannot be bound to anything.
We can read ?- woman(X) as a query ``is there a woman?'' and this query failed. Yet we know that woman(jane) succeeds. Therefore, this form of negation is not at all like logical negation.The problem can be highlighted using predicate logic. The query woman(X) is interpreted as
which, logically, is equivalent tox
man(x)
Now Prolog solves this goal in a manner roughly equivalent to
x man(x)
The only time we get something like the desired result if there is no existentially quantified variable in the goal. That is, whenever
x man(x)
\+/1 is used then make sure that its argument is bound at the time it is called.
Also, note that \+(\+(man(X))) is not identical to man(X)
since the former will succeed with X unbound
while the latter will succeed with
X bound, in the first instance, to jim.
This is the basis of a well known Prolog programming `trick' --- i.e. it is a technique which is frowned upon by purists. The idea is to test whether, for example, two terms will unify without the effect of binding any variables. The goal\+(\+(X=2)) will succeed without binding X to 2. The meaning is roughly X would unify with 2.