zbMATH — the first resource for mathematics

Real quantifier elimination is doubly exponential. (English) Zbl 0663.03015
The authors show that quantifier elimination over the first-order theory of real-closed fields can require doubly-exponential space (and hence time) and show that this doubly-exponential behaviour is intrinsic to the problem. This result has already been proved by Weispfenning by a completely different method in 1985, but the method of the paper is of independent interest.
Reviewer: Li Xiang

03C10 Quantifier elimination, model completeness, and related topics
68Q25 Analysis of algorithms and problem complexity
12L05 Decidability and field theory
68W30 Symbolic computation and algebraic computation
12D99 Real and complex fields
Full Text: DOI
[1] Ben-Or, M.; Kozen, D.; Reif, J., The complexity of elementary algebra and geometry, J. comput. syst. sci, 32, 251-264, (1986) · Zbl 0634.03031
[2] Collins, G.E., Quantifier elimination for real closed fields by cylindrical algebraic decomposition, (), 134-183, MR 55 #771
[3] Davenport, J.H., Computer algebra for cylindrical algebraic decomposition, () · Zbl 0651.68043
[4] Heintz, J., Definability and fast quantifier elimination in algebraically closed fields, Theor. comp. sci., 26, 239-277, (1983), MR 85a:68061 · Zbl 0546.03017
[5] McCallum, S., An improved projection operation for cylindrical algebraic decomposition, (), 277-278, (Springer Lecture Notes in Computer Science 204)
[6] McCallum, S., An improved projection operation for cylindrical algebraic decomposition, (), Feb 1985
[7] Tarski, A., A decision method for elementary algebra and geometry, (1951), Univ. Cal. Press, Berkeley, 1951, MR 10 #499 · Zbl 0044.25102
[8] Weispfenning, V., (), (revised March 1986)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.