AbstractIn this paper, a new algorithm for performing quantifier elimination from first order formulas over real closed fields is given. This algorithm improves the complexity of the asymptotically fastest algorithm for this problem, known to this date. A new feature of this algorithm is that the rule of the algebraic part (the dependence on the degrees of the input polynomials) and the combinatorial part (the dependence on the number of the polynomials) are separated. Another new feature is that the degrees of the polynomials in the equivalent quantifier-free formula that is output, are independent of the number of input polynomials. As special cases of this algorithm, new and improved algorithms for deciding a sentence in the first order theory over real closed fields, and also for solving the existential problem in the first order theory over real closed fields, are obtained.
The abstract is also available as a LaTeX file, a DVI file, or a PostScript file.
Categories and Subject Descriptors: F.4.3 [Mathematical Logic and Formal Languages]: Formal Languages -- decision problems
General Terms: Algorithms, Theory
Additional Key Words and Phrases: Quantifier elimination, real closed fields, Tarski-Seidenberg principle
Selected papers that cite this one
- Saugata Basu. An improved algorithm for quantifier elimination over real closed fields. In 38th Annual Symposium on Foundations of Computer Science, pages 56-65, Miami Beach, Florida, 20-22 October 1997. IEEE.
- Saugata Basu. On bounding the Betti numbers and computing the Euler characteristic of semi-algebraic sets. In Proceedings of the Twenty-Eighth Annual ACM Symposium on the Theory of Computing, pages 408-417, Philadelphia, Pennsylvania, 22-24 May 1996.
- S. Basu, R. Pollack, and M.-F. Roy. Computing roadmaps of semi-algebraic sets (extended abstract). In Proceedings of the Twenty-Eighth Annual ACM Symposium on the Theory of Computing, pages 168-173, Philadelphia, Pennsylvania, 22-24 May 1996.
- Leonid Khachiyan and Lorant Porkolab. Computing integral points in convex semi-algebraic sets. In 38th Annual Symposium on Foundations of Computer Science, pages 162-171, Miami Beach, Florida, 20-22 October 1997. IEEE.
Selected references
- S. Basu, R. Pollack, and M.-F. Roy. On the combinatorial and algebraic complexity of quantifier elimination. In 35th Annual Symposium on Foundations of Computer Science, pages 632-641, Santa Fe, New Mexico, 20-22 November 1994. IEEE.
- Michael Ben-Or, Dexter Kozen, and John Reif. The complexity of elementary algebra and geometry. Journal of Computer and System Sciences, 32(2):251-264, April 1986.
- John Canny. Some algebraic and geometric computations in PSPACE. In Proceedings of the Twentieth Annual ACM Symposium on Theory of Computing, pages 460-467, Chicago, Illinois, 2-4 May 1988.
- M. Coste and M. F. Roy. Thom's lemma, the coding of real algebraic numbers and the computation of the topology of semi-algebraic sets. Journal of Symbolic Computation, 5(1/2):121-130, February/April 1988.
- D. Yu Grigor[?]ev. Complexity of deciding tarski algebra. Journal of Symbolic Computation, 5(1/2):65-108, February/April 1988.
- D. Yu. Grigor[?]ev and N. N. Vorobjov, Jr. Solving systems of polynomial inequalities in subexponential time. Journal of Symbolic Computation, 5(1/2):37-64, February/April 1988.
- Pascal Koiran. A weak version of the Blum, Shub & Smale model. In 34th Annual Symposium on Foundations of Computer Science, pages 486-495, Palo Alto, California, 3-5 November 1993. IEEE.
- J. Renegar. On the computational complexity and geometry of the first-order theory of the reals, part III: Quantifier eliminiation. Journal of Symbolic Computation, 13(3):329-352, March 1992.
- M. F. Roy and A. Szpirglas. Complexity of the computation on real algebraic numbers. Journal of Symbolic Computation, 10(1):39-52, July 1990.