🚀 go-pugleaf

In article <2221@cs-spool.calgary.UUCP> 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(...).
>Warning there can be a lot of these clauses: n1*n2*n3*...nm to be precise.
>Also I have assumed the heads of teh clauses contain only free variables
>so the aij(...) may be equality(=). To avoid a circular definition of not(_=_)
>this needs to be done explicitly.  Given a finite Herbrand Universe
>there are only a finite (but possibly large) number of pairs of things that
>are not equal so this too can be written down (it is however different for
>each program).

If some of the clauses for p above have right-free variables, i.e
variables that occur in the body but not in the head, the above approach
does not work. Consider for instance the following example (due to
Barbuti el. al. [1])

Let P be the program
	s(X,Y) :- p(X,Y,Z).
	p(X,Y,Z) :- q(X,Y,Z), r(X,Y,Z).
	q(X,Y,Z) :- X = b.
	q(X,Y,Z) :- Z = b.
	r(X,Y,Z) :- Z = a.
	r(X,Y,Z) :- Y = b.
	
With the above approach (as I understand it) you get the following
clauses, where the intended meaning of ns is not s
	ns(X,Y) :- np(X,Y,Z).
	np(X,Y,Z) :- nq(X,Y,Z).
	np(X,Y,Z) :- nr(X,Y,Z).
	nq(X,Y,Z) :- not_eq(X,b), not_eq(Z,b).
	nr(X,Y,Z) :- not_eq(Z,a), not_eq(Y,b).
	not_eq(a,b).
	not_eq(b,a).

Let P' be the program obtained by adding the above clauses to P. Now,
both s(a,b) and ns(a,b) are logical consequences of P'! The problem is
that the variable Z in the the clause for s becomes universally
quantified when this clause is "negated", and this is not taken care of
in the above approach.

[1] Barbuti, Mancarella, Pedreschi and Turini: A Transformational
Approach to Negation in Logic Programming. To appear in Journal of Logic
Programming 


		Torbjorn Naslund
		Dept. of Computer and Information Science
		Linkoping University
		S-581 83 Linkoping
		Sweden