<p>The theory of <a href="http://en.wikipedia.org/wiki/Real_closed_field" rel="nofollow">real closed fields</a> (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.</p>

<p>By <a href="http://en.wikipedia.org/wiki/Real_closed_field#Model_Theory%3a_decidability_and_quantifier_elimination" rel="nofollow">Tarski's quantifier elimination</a> for RCF this can be computed. Tarski's algorithms complexity is <a href="http://en.wikipedia.org/wiki/NONELEMENTARY" rel="nofollow">non-elementary</a> and there is a <a href="http://mathworld.wolfram.com/QuantifierElimination.html" rel="nofollow">doubly exponential lowerbound</a> for the problem.</p>

<p>A more efficient algorithm than Tarski's algorithm is given by <a href="http://www.math.purdue.edu/~sbasu/" rel="nofollow">Saugata Basu</a> "<a href="http://dx.doi.org/10.1109/SFCS.1997.646093" rel="nofollow">An Improved Algorithm for Quantifier Elimination Over Real Closed Fields</a>", FOCS 1997 (which seems to be almost optimal, see Theorem 1) (a draft of the paper is available <a href="http://www.math.purdue.edu/~sbasu/focs97.ps" rel="nofollow">here</a>). </p>

<p>Also check Saugata Basu, "<a href="http://www.math.purdue.edu/~sbasu/journalacm.ps" rel="nofollow">New Results on Quantifier Elimination Over Real Closed Fields and Applications to Constraint Databases</a>", Journal of the ACM, 1999. </p>

CC BY-SA 3.0
2011-08-15T23:35:38.657Z
(The Basu link doesn't seem to work.)
François G. Dorais
CC BY-SA 3.0
2011-08-15T19:32:47.673Z
2011-08-16T04:52:39.013Z
2011-08-16T04:52:39.013Z
Kaveh
<p>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?</p>

<cc.complexity-theory><lo.logic><model-theory>
Time/Space Requirements of Verifying or Falsifying a First-Order Statement
Jesse Stern
# Time/Space Requirements of Verifying or Falsifying a First-Order Statement

(Asked by: username_0 on 2011-08-15)

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?

**Tags:** cc.complexity-theory, lo.logic, model-theory

---

## 1 answers

### Answer by username_1 on 2011-08-15. Score: 8 | Accepted answer

The theory of [real closed fields](http://en.wikipedia.org/wiki/Real_closed_field) (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](http://en.wikipedia.org/wiki/Real_closed_field#Model_Theory%3a_decidability_and_quantifier_elimination) for RCF this can be computed. Tarski's algorithms complexity is [non-elementary](http://en.wikipedia.org/wiki/NONELEMENTARY) and there is a [doubly exponential lowerbound](http://mathworld.wolfram.com/QuantifierElimination.html) for the problem.

A more efficient algorithm than Tarski's algorithm is given by [Saugata Basu](http://www.math.purdue.edu/~sbasu/) "[An Improved Algorithm for Quantifier Elimination Over Real Closed Fields](http://dx.doi.org/10.1109/SFCS.1997.646093)", FOCS 1997 (which seems to be almost optimal, see Theorem 1) (a draft of the paper is available [here](http://www.math.purdue.edu/~sbasu/focs97.ps)).

Also check Saugata Basu, "[New Results on Quantifier Elimination Over Real Closed Fields and Applications to Constraint Databases](http://www.math.purdue.edu/~sbasu/journalacm.ps)", Journal of the ACM, 1999.

> **Comments:**
> **username_2**: (The Basu link doesn't seem to work.)  

---

