> The assume database can simultaneously keep mutually
> contradictive statements. This is bad. From a pair of
> contradictive statements one can infer any desirable
> statement by applying only correct inference rules. Thus, it
> is very dangerous to do elements of automated inference
> in Maxima.
As has been mentioned before, Maxima's inequality package is quite weak.
It allows contradictory assertions for the simple reason that it does
not know that they are contradictory. (A simpler example is
assert(a+b>c,a+b<c).)
Indeed, I believe that the only case the inequality package handles
completely is comparison of symbols to symbols (a>b), and symbols to
constants (a>0; also 2*a>1 ==> a>1/2). It fails even on extremely
simple cases beyond that. For example: assume(a>0,b>2*a); sign(a)=>POS
(OK); sign(2*a)=>POS (OK); sign(b)=> PNZ (!!!)
Obviously, one can do much better than that, and it would be wonderful
if you could contribute code to improve the inequality package, perhaps
with a general inference engine.
HOWEVER, no matter how well Maxima does, it will never be able to detect
all contradictions. So what do you do? Do you only allow assertions
that Maxima can prove not to be contradictory? That would be far too
restrictive (though it is of course desirable that it report on
contradictory assertions *when* it detects them). For that matter, it
is *useful* to allow contradictory assertions when pursuing a reductio
ad absurdum argument. So it is not only *unavoidable* that Maxima will
allow contradictory assertions, but actually *desirable* that it do so.
-s