Path: utzoo!attcan!utgpu!jarvis.csri.toronto.edu!clyde.concordia.ca!uunet!mcsun!inria!ilog!puget
From: puget@ilog.UUCP (Francois Puget)
Newsgroups: comp.lang.prolog
Subject: Re: Fun. vs. Logic
Message-ID: <6396@ilog.UUCP>
Date: 14 Dec 89 13:34:41 GMT
References: <11500018@hpldola.HP.COM> <11500020@hpldola.HP.COM> <2221@cs-spool.calgary.UUCP>
Reply-To: puget@ilog.UUCP (Jean-Francois Puget)
Organization: ILOG, Paris, France
Lines: 114

in a previous article cleary@cpsc.ucalgary.ca (John Cleary) writes

>There is a simple translation of negation to first order logic that requires
>a correct implementation of not equals.  Given a predicate say p(X1,...) which
>is called somewhere in the form not(p(Y1...)) then the call can be replaced
>by a positive call np(Y1,...) where the definition of np can be derived
>systematicly from that for p.
>If p is defined as follows:
>
>	p(X1,...) :- a11(...), ..... a1n1(....)
>        p(X1,...) :- a21(...), ......a2n2(....)
>	...
>	p(X1,...) :- am1(...), ..... amnm(....)
>
>then np is defined as
>
>	np(X1,...):- not(a11(...)), not(a21(...)), ... not(am1(...))
>	np(X1,...):- not(a11(...)), not(a21(...)), ... not(am2(...))
>        ....
>	np(X1,...):- not(a1n1(...)), not(a21(...)), ... not(amnm(...))
>
>where each of the not(aij(..)) can be further translated or if they
>are of the form not(not(q(...)) replced by q(...).

This is unfortunately incorrect. Let us take a simple example

	member(X,Y):- Y=[X|A].
	member(X,Y):- Y=[B|C], member(X,C).

the proposed solution would define the negation of member as

	n_member(X,Y):- not(Y=[X|A)), not(Y=[B|C]).
	n_member(X,Y):- not(Y=[X|A]), not(member(X,C).

Well, if anybody is convinced that this is a good definition of n-member,
i would like some explanations.

>
... deleted ...
>I am not entirely sure of the theoretical status of this translation.

You are right

>It assumes that the completion of the program is what you really meant 

No

The completion would give 

(1)	forall X,Y not(member(X,Y)) <-
	   ((forall A,A' not(X=A') or not(Y=[A'|A]))
	    and
	    (forall A'',B,C, not(X=A'') or not(Y=[B|C]) or not(member(A'',C))))
	
You see that the quantifications of variables are very important here since 
some of them are universally quantified in the 'body' of the above formula.
(In fact the completion gives an equivalence instead of the implication above).
A good treatement of this subject can be found in (Shepherdson, 88).
Beside quantifications, the proposed solution ignores shared variables.
	
>and gives the usual semantics for stratified programs as near as I can tell.
>For nostratified programs, for example:
>
>	p:- not(p)
>
>the translated program is:
>	p:- not_p
>
>	not_p:-p.
>which would conclude that both p and not_p are false.  So in there is no 
>guarantee that the result will be consistent in these cases.

I can add that for Definite clause programs, such as pure prolog, the 
completion is consistent (Shepherdson, 88).

>The standard minimal meta-interpreter for Prolog can be extended to give this
>type of behavior as follows.  Assume that the program is represented by the 

... deleted ...

the proposed program is not justified on logical grounds. I have develloped a 
system that transforms the completion into a set of definite clauses 
(puget, 89). In the member case it produces the following program for n-member

	n_member(X,[]).
	n_member(X,[Y|Z):-not(X=Y),n_member(X,Z).

The principle is to use the equality theory defined in the completion to 
simplify the formula (1) above. This is done with a rewrite system similar to the disunification algorithm introduced in (Comon, 88).

A similar approach is described in (Lugiez, 89), and in (Barbuti et al, 88). These approaches are not perfect : all the universal cannot be eliminated in the body of the formulas. All those approaches assume that an implementation of 
not-equal is given. In other terms they use a cosure domain axiom.

I give here the references from memory. 

(Comon, 88) Disunification: theorie et applications
	These, Universite de Grenoble, December 88.
There are two papers in English. I will [post the references later.

Maher and Lassez have studied this also.

(Lugiez, 89) A deductive Procedure for first order formulas, in proceedings of
ICLP 89.

(Puget. 89) Explication d'echecs en Prolog, in proceedings of SPLT'89, 
march 89, tregastel, France. (in french).

(Shepherdson, 88) Negation in logic programming, in Foundation of logic 
programming and deductive databases, Minker and Gallaire (eds), 88.

The facts expressed above are my beliefs and any error are mine.

Jean-Francois Puget
email; puget@lri.lri.fr