> Logical negation is not so simple. In IEEE floating point number
> comparisons, NotANumbers a,b ... a>b is false [etc.]
Yes, and if NaNp(a) or a=Inf, then a-a is not equal to 0, either. But
Maxima assumes standard real numbers, not intervals, IEEE floats, fuzzy
numbers, non-standard reals with infinitesimals, point sets, etc.
Though it would be nice to be able to perform symbolic calculations on
various non-standard arithmetics, Maxima pervasively assumes
trichotomic, Archimedean, associative, etc. arithmetic. In fact, even
for the few non-standard objects it *does* support, it often gets it
wrong, e.g. INF-INF => 0. I'm not saying this can't change, just that
there's nothing unique about relationals being limited to the standard
reals in current Maxima.
> if a<b is "not known to be true" that does not
> mean it is "known to be false".
With prederror:true (the default), I believe it is the case that (not
is(E)) is always equivalent to is(not E). Following the usual
convention, I am assuming that error returns mean that the whole
calculation is undefined.
Only in the three-valued form of IS (with prederror:false) is it
possible to ask the question "can Maxima show this to be true":
known_true(x):= block([prederror:false],is(is(x)=true) $
known_false(x):= block([prederror:false],is(is(x)=false)$
And sure enough, known_true(x=1) is not equivalent to not
known_false(x#1), although is(x=1) is equivalent to not is(x#1).
Boolean operators in Maxima are currently all programming operators, and
not mathematical operators. So only the component relations are
evaluated mathematically. For example, is(x>0 or x<1) returns FALSE,
because it is equivalent to is(is(x>0) or is(x<1)), which corresponds to
the mathematical statement ForAll[x](x>0) or ForAll[x](x<1) rather than
the mathematical statement ForAll[x](x>0 or x<1). In fact, there is
currently no way of expressing that last statement in Maxima at all.
Well, I could write more completely, or more cogently, and maybe even
both, but that's enough for now!
> We could consider reading OTTER, a theorem prover, into
> Maxima, and have something that was state of the art, instead
> of cooking up our own.
I have not looked at Otter, but of course we should take advantage of
whatever existing tools exist, as long as we create a consistent, usable
system.
-s