A Sound/Complete Implementation of Negation As Failure?

Appeared in Volume 9/1, February 1996

Keywords: negation.

poole@cs.ubc.ca
David Poole
8th September 1995

I am looking for a Prolog-like language that correctly implements negation as failure, according to Clark's semantics, the stable model semantics, or the well founded semantics. I am only interested in acyclic programs, so I am not concerned about cases where these semantics differ. I am not satisfied with a program that delays negation as failure with free variables, and flounders on programs that have free variables in the negation.

I am constructing a list of terms of the form p(X,Y) and want to enforce the constraint that p/2 is functional (if the X's agree then the Y's must agree).

Here is a specification of the program:

functional(L) :-
    \+ notfun(L).
notfun(L) :-
    member(p(X,Y1),L),
    member(P(X,Y2),L),
    Y1 \= Y2.

member(X,[X|_]).
member(X,[_|Z]) :-
    member(X,Z).

% X \= Y is true if X and Y are not equal
X \= Y :-
    \+ X=Y.

I expect the following results (all of which follow from the above program using Clark's completion, the stable model semantics, or ... )

? functional([p(a,b),p(b,c),p(a,d)])
fails

? functional([p(a,b),p(b,c),p(d,d)])
succeeds

? functional([p(a,b),p(b,c),p(a,X)])
succeeds with X=b

? functional([p(a,Y),p(b,c),p(a,X)])
succeeds with Y=X

? functional([p(a,b),p(Z,c),p(c,d)])
succeeds with the costraint that Z \= a and Z \= c

? functional([p(a,Y),p(Z,c),p(a,X)])
succeeds with two answers:
  X=Y & Z\=a
  Z=a X=Y=c
(or some other representation of the constraints on these)

lee@cs.mu.oz.au
Lee Naish
25th September 1995

The key to getting functional/1 to work in complex modes (e.g., non-ground) is to reduce the negation to inequality. Some logic programming systems will do this for you (e.g., constructive negation); in some you have to do it yourself. In NU-Prolog (and various other systems which support sound inequality), you can code the above specification as follows:

:- functional(Ps) when Ps.
functional([]).
functional(p(X, Y).Ps) :-
    consistent(X, Y, Ps),
    functional(Ps).

:- consistent(_, _, Ps) when Ps.
consistent(_, _, []).
consistent(X, Y, p(X, Y).Ps) :-
    consistent(X, Y, Ps).
consistent(X, Y, p(X1, _).Ps) :-
    X ~= X1,
    consistent(X, Y, Ps).

This works fine for all the queries given above, and also (due to the when declarations) some others in which the list is not of determinate length. For example:

?- functional([p(a, b), p(b, c), p(a, d)|Z]).
fail.