[m-dev.] Re: diff: Fix problem with quantifiers and double negation

[Andrew Bromage]

G'day all.

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

> >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 ;-),

Lee Naish replied:

> 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.

It doesn't look right on the face of it.  This goal:

	\+ (
		produce(X :: out) is det,
		test(X :: in) is semidet
	)

does not correctly transform into:

	(
		\+ (produce(X :: out) is det)
	;
		\+ (test(X :: in) is semidet)
	)

Cheers,
Andrew Bromage