Prolog negation and logical negation

Question

Assume we have the following program:

a(tom). 
v(pat).

and the query (which returns false):

\+ a(X), v(X).

When tracing, I can see that X becomes instantiated to tom, the predicate a(tom) succeeds, therefore \+ a(tom) fails.

I have read in some tutorials that the not (\+) in Prolog is just a test and does not cause instantiation.

1. Could someone please clarify the above point for me? As I can see the instantiation.

2. I understand there are differences between not (negation as failure) and the logical negation. Could you refer a good article that explains in which cases they behave the same and when do they behave different?

Answer 1

WRT point 2, Wikipedia article seems a good starting point.

You already experienced that understanding NAF can be difficult. Part of this could be because (logical) negation it's inherently difficult to define even in simpler contest that predicate calculus (see for instance Russel's paradox), and part because the powerful variables of Prolog are domed to keep the actual counterexamples of failed if negated proofs. See if you can understand the actual library definition of forall/2 (please read the documentation, it's synthetic and interesting) that's the preferred way to run a failure driven loop:

%%  forall(+Condition, +Action)
%
%   True if Action if true for all variable bindings for which Condition
%   if true.

forall(Cond, Action) :-
    \+ (Cond, \+ Action).

I remember the first time I saw it, it looked like magic...

edit about a tutorial, I found, while 'spelunking' my links collection, a good site by J.R.Fisher. It's full of interesting stuff, just a pity it's a bit terse in explanations, requiring the student to answer itself with frequent execises. See the paragraph 2.5, devoted to negation by failure. I think you could also enjoy section 3. How Prolog Works

Answer 2

Great question.

Short answer: you stumbled upon "floundering".

The problem is that the implementation of the operator \+ only works when applied to a literal containing no variables, i.e., a ground literal. It is not able to generate bindings for variables, but only test whether subgoals succeed or fail. So to guarantee reasonable answers to queries to programs containing negation, the negation operator must be allowed to apply only to ground literals. If it is applied to a nonground literal, the program is said to flounder. link

If you invert the query

v(X), \+ a(X).

You'll get the right answer. Some implementations or meta interpreter detect floundering goals and delay them until all the variables are ground.

About your point 1), you see the instantiation inside the NAF tree. What happens there shouldn't affect variables that are outside (in this case in v(X)). Prolog often acts in the naive way to avoid inefficiencies. In theory it should just return an error instead of instantiating the variable.

2) This is my favourite article on the topic: Nonmonotonic Logic Programming.