diff: Fix problem with quantifiers and double negation

Lee Naish lee at cs.mu.OZ.AU
Wed Jun 24 14:25:08 AEST 1998


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



More information about the developers mailing list