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

Zoltan Somogyi zs at cs.mu.OZ.AU
Fri Jun 12 15:35:18 AEST 1998


> +:- pred all_negated(list(hlds_goal), list(hlds_goal)).
> +:- mode all_negated(in, out) is semidet.
> +
> +all_negated([], []).
> +all_negated([not(Goal) - _ | NegatedGoals], [Goal | Goals]) :-
> +	all_negated(NegatedGoals, Goals).

This will not catch cases where the conjunction is nested. I believe nested
conjunctions can occur at that stage of the processing.

Is there any reason why we shouldn't also do the converse transformation,
i.e. turning the negation of a disjunction in which each disjunct is a
negated goal into the conjunction of the unnegated disjuncts? E.g.
~(~p or ~q) ===> p, q.

Nested disjunctions can also occur.

Zoltan.



More information about the developers mailing list