ok@edai.UUCP (Richard O'Keefe) (09/07/83)
Here is an argument in favour of the Dec-10 interpretation. The example I gave in Not.Hlp to show that there was a problem was about bachelors, this one is about widowers. Suppose we are writing some sort of pension program, and one of the rules is entitlement(Man, supp(1)) :- male(Man), age(Man, Age), Age >= 65, \+ (wife(Man,Woman), dead(Woman)), ... The reading we want here is not (exists Woman) (wife(Man,Womand) and dead(Woman)). If we fold those two goals into a new predicate, widower(Man) :- wife(Man, Woman), dead(Woman). then the original negation is exactly equivalent to \+ widower(Man). Of course this only holds for cut-free subformulae, but arguments about ordering are mainly cocerned with that case anyway. If you take the view that the Dec-10 et al interpreters take, which is that negation flips the quantifier poolarity just like it does in logic. flips the quantifier polarity just like it does in logic, this substitution property holds. Such properties are very important for program transformation. If we take the other interpretation, which binds Woman, we are asking is there a Woman who is not the wife of Man or is not dead. Note that *anything* which isn't dead will do. Whether or not this interpretation is desirable, it isn't the interpretation that calling \+ widower(Man) provides, which clearly can't bind Woman to anything. I haven't yet had a chance to use MU Prolog, but from reading the manual it looks as though the negated goals would be indefinitely delayed, as the Woman variable would be unbound, and there are no other goals which could bind it. While I prefer the Dec-10 solution in this particular case, the MU Prolog solution appearnm/aw