zbMATH — the first resource for mathematics

On the computational complexity and geometry of the first-order theory of the reals. III: Quantifier elimination. (English) Zbl 0798.68073
Summary: This series of papers [part I, ibid. 13, No. 3, 255-299 (1992; Zbl 0763.68042); part II, ibid. 13, No. 3, 301-327 (1992; Zbl 0763.68043)] presents a complete development and complexity analysis of a decision method, and a quantifier elimination method, for the first order theory of the reals. The complexity upper bound which are established are the best presently available, and both for sequential and parallel computation, and both for the bit model of computation and the real number model of computation; except for the bounds pertaining to the sequential decision method in the bit model of computation, all bounds represent significant improvements over previously established bounds.

68Q25 Analysis of algorithms and problem complexity
14P10 Semialgebraic sets and related spaces
03C10 Quantifier elimination, model completeness, and related topics
03B25 Decidability of theories and sets of sentences
PDF BibTeX Cite
Full Text: DOI
[1] Ben-Or, M.; Kozen, D.; Reif, J., The complexity of elementary algebra and geometry, J. computer syst. sci., 32, 251-264, (1986) · Zbl 0634.03031
[2] Brown, W.; Traub, J., On Euclid’s algorithm and the theory of subresultants, J. association for computing machinery, 18, 505-514, (1971) · Zbl 0226.65041
[3] Collins, G., Subresultants and reduced polynomial remainder sequences, J. association for computing machinery, 14, 128-142, (1967) · Zbl 0152.35403
[4] Csanky, L., Fast parallel matrix inversion algorithms, SIAM journal on computing, 5, 618-623, (1976) · Zbl 0353.68063
[5] Tarski, A., A decision method for elementary algebra and geometry, (1951), University of California Press · Zbl 0044.25102
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.