Though L.Berman proved that the problem of verifying or falsifying any first-order statement about real numbers that uses addition and comparison but not multiplication is in EXPSPACE. Has it been shown how much time or space you would nee to verify or falsify any first-order statement about real numbers that uses addition comparison AND multiplication?
$\begingroup$
$\endgroup$
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
1
The theory of real closed fields (RCF) is complete for the first order theory of real numbers in the language you described. Therefore it is equivalent to checking if RCF proves the formula.
By Tarski's quantifier elimination for RCF this can be computed. Tarski's algorithms complexity is non-elementary and there is a doubly exponential lowerbound for the problem.
A more efficient algorithm than Tarski's algorithm is given by Saugata Basu "An Improved Algorithm for Quantifier Elimination Over Real Closed Fields", FOCS 1997 (which seems to be almost optimal, see Theorem 1) (a draft of the paper is available here).
Also check Saugata Basu, "New Results on Quantifier Elimination Over Real Closed Fields and Applications to Constraint Databases", Journal of the ACM, 1999.
-
$\begingroup$ (The Basu link doesn't seem to work.) $\endgroup$ Aug 15, 2011 at 23:35