I am working on a program analysis tool for a research project as part
of my graduate studies, and I need a decision procedure for first
order arithmetic. I need to be able to decide whether expressions
like:
EXISTS x: x > 0 AND FORALL a: x*a >= 0
are true.
Tarski's theorem says that when the variables range over real numbers,
quantifier elimination implies the decidability of such expressions.
Ideally I would also like to get values for existentially quantified
variables if the expression is true (e.g., x = 1, although the example
is false), but this is not essential.
I would like to use Maxima because it is open source and free, but I
have not been able to figure out whether Maxima includes the necessary
expressive power to solve such expressions. Can anyone tell me
either: that this is not possible, or, if it is possible, how to do
it? Thanks.
--Gary