×

Elementary recursive quantifier elimination based on Thom encoding and sign determination. (English) Zbl 1373.14060

In the paper under review, the authors describe a new quantifier elimination algorithm for real closed fields based on Thom encoding and sign determination whose complexity is elementary recursive. What is important, the proof of its correctness is entirely based on algebra and does not involve the notion of connected components of semialgebraic sets: for all previously existing elementary recursive methods, the proofs of correctness of the algorithms had been based on geometric properties of semialgebraic sets. The development of algebraic proofs is very important in the field of constructive algebra. In particular, it is important to provide an elementary recursive algorithm for quantifier elimination over real closed fields, suitable for being formally checked by a proof assistant such as Coq.

MSC:

14P10 Semialgebraic sets and related spaces
03C10 Quantifier elimination, model completeness, and related topics
14Q20 Effectivity, complexity and computational aspects of algebraic geometry
12D15 Fields related with sums of squares (formally real fields, Pythagorean fields, etc.)

Software:

Coq
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Basu, S.; Pollack, R.; Roy, M.-F., On the combinatorial and algebraic complexity of quantifier elimination, J. ACM, 43, 1002-1045 (1996) · Zbl 0885.68070
[2] Basu, S.; Pollack, R.; Roy, M.-F., Algorithms in Real Algebraic Geometry, Algorithms Comput. Math., vol. 10 (2006), Springer-Verlag: Springer-Verlag Berlin · Zbl 1102.14041
[3] Basu, S.; Pollack, R.; Roy, M.-F., Algorithms in Real Algebraic Geometry, Algorithms Comput. Math., vol. 10 (2006), New online version available at · Zbl 1102.14041
[4] Ben-Or, M.; Kozen, D.; Reif, J., The complexity of elementary algebra and geometry, J. Comput. Syst. Sci., 18, 251-264 (1986) · Zbl 0634.03031
[5] Berkowitz, S., On computing the determinant in small parallel time using a small number of processors, Inform. Process. Lett., 18, 147-150 (1984) · Zbl 0541.68019
[6] Canny, J., Improved algorithms for sign determination and existential quantifier elimination, Comput. J., 36, 5, 409-418 (1993) · Zbl 0789.68079
[8] Cohen, P. J., Decision procedures for real and p-adic fields, Comm. Pure Appl. Math., 22, 131-151 (1969) · Zbl 0167.01502
[9] Cohen, C.; Mahboubi, A., Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination, Log. Methods Comput. Sci., 8, 1:02 (2012) · Zbl 1241.68096
[10] Collins, G., Quantifier Elimination for real closed fields by cylindric algebraic decomposition, (Second GI Conference on Automata Theory and Formal Languages. Second GI Conference on Automata Theory and Formal Languages, Lecture Notes in Comput. Sci., vol. 33 (1975), Springer-Verlag: Springer-Verlag Berlin), 134-183 · Zbl 0318.02051
[11] Coste, M.; Roy, M.-F., Thom’s lemma, the coding of real algebraic numbers and the computation of the topology of semi-algebraic sets, J. Symbolic Comput., 121-129 (1988) · Zbl 0689.14006
[12] Cox, D.; Little, J.; O’Shea, D., Ideals, Varieties, and Algorithms. An Introduction to Computational Algebraic Geometry and Commutative Algebra, Undergrad. Texts Math. (2007), Springer: Springer New York · Zbl 1118.13001
[13] Davenport, J. H.; Heintz, J., Real quantifier elimination is doubly exponential, J. Symbolic Comput., 5, 29-35 (1988) · Zbl 0663.03015
[14] Grigoriev, D., Complexity of deciding Tarski algebra, J. Symbolic Comput., 5, 65-108 (1988) · Zbl 0689.03021
[15] Grigoriev, D.; Vorobjov, N., Solving systems of polynomial inequalities in subexponential time, J. Symbolic Comput., 5, 37-64 (1988) · Zbl 0662.12001
[16] Hörmander, L., The Analysis of Linear Partial Differential Operators, 364-367 (1983), Springer: Springer Berlin, Heidelberg, New-York · Zbl 0521.35001
[17] Lojasiewicz, S., Ensembles Semi-Analytiques (1965), Institut des Hautes Etudes Scientifiques
[19] Monk, L. G., Elementary-Recursive Decision Procedures (1975), UC Berkeley, PhD thesis
[20] Renegar, J., On the computational complexity and geometry of the first-order theory of the reals. I-III, J. Symbolic Comput., 13, 255-352 (1992) · Zbl 0798.68073
[21] Seidenberg, A., A new decision method for elementary algebra, Ann. of Math., 60, 365-374 (1954) · Zbl 0056.01804
[22] Tarski, A., A Decision Method for Elementary Algebra and Geometry (1951), University of California Press: University of California Press Berkeley and Los Angeles, CA · 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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.