diff: Fix problem with quantifiers and double negation

[Lee Naish]

Fergus Henderson <fjh at cs.mu.OZ.AU> writes:


> > >	3.	`~(if P then Q else R)' ===> `if P then ~Q else ~R'.
> > 
> > >	4.	`~(P, Q, ...)' ===> `~NotP ; ~NotQ ; ...' iff
> > >			`~P' ===> `NotP', and `~Q' ===> `NotQ', and ...

>Sorry, I made a mistake there -- I meant

>	4.	`~(P, Q, ...)' ===> `NotP ; NotQ ; ...' iff
>			`~P' ===> `NotP', and `~Q' ===> `NotQ', and ...

> > 3 and 4 above - they are wrong.

>For those of us who still haven't had the first coffee of the day ;-),

Like me:-)  I think 3. is probably ok (maybe I was getting confused with
negating P).  The correctness of 4. depends very much on what rules are
used for implicit quantification and what restrictions are placed on
modes.  For example, using the current Mercury implicit quantification
scheme its not sufficient to just check the modes after transformation:

p(1).

	~(~p(X), ~p(X))	% ~ some [X] (~p(X), ~p(X)) False, ill-moded
===>
	(p(X) ; p(X))	% True, well-moded

	lee