For questions regarding the concept of negation as failure in logic programming. Please include all relevant tags on your question; e.g., [prolog], [answer-set-programming], etc.
Negation as failure (NAF) is a non-monotonic inference rule in logic programming, used to derive not p from failure to derive p. The adoption of this kind of negation is strictly related to the closed-world assumption.
For instance, let us consider the following Prolog program:
grandpa(X,Z) :- father(X,Y), parent(Y,Z).
parent(X,Y) :- father(X,Y).
parent(X,Y) :- mother(X,Y).
father(a,b).
mother(b,c).
For answering to the question ?- not grandpa(a,b)., the program will expand the tree having as root grandpa(a,b), from which it follows father(a,X), parent(X,b) and, non-deterministically, father(X,b) and mother(X,b). Both the branches indeed will fail: the first one because it does not exist any X satisfying father(a,X) and father(X,b) at the same time; the second one because mother(X,b) doesn't unify with any fact in the extensional database.
If follows that grandpa(a,b) will be considered false and the answer to
?- not grandpa(a,b).
will be
yes.
