Abstract:
We describe a new quantifier elimination algorithm for real closed fields based on Thom encoding and sign determination. The complexity of this algorithm is elementary recursive and its proof of correctness is completely algebraic. In particular, the notion of connected components of semialgebraic sets is not used. © 2017 Elsevier B.V.
Registro:
Documento: |
Artículo
|
Título: | Elementary recursive quantifier elimination based on Thom encoding and sign determination |
Autor: | Perrucci, D.; Roy, M.-F. |
Filiación: | Departamento de Matemática, FCEN, Universidad de Buenos Aires, IMAS UBA-CONICET, Ciudad Universitaria, Buenos Aires, 1428, Argentina IRMAR (UMR CNRS 6625), Université de Rennes 1, Campus de Beaulieu, Rennes cedex, 35042, France
|
Palabras clave: | Quantifier elimination; Real closed fields; Sign determination; Thom encoding |
Año: | 2017
|
Volumen: | 168
|
Número: | 8
|
Página de inicio: | 1588
|
Página de fin: | 1604
|
DOI: |
http://dx.doi.org/10.1016/j.apal.2017.03.001 |
Título revista: | Annals of Pure and Applied Logic
|
Título revista abreviado: | Ann. Pure Appl. Logic
|
ISSN: | 01680072
|
CODEN: | APALD
|
Registro: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_01680072_v168_n8_p1588_Perrucci |
Referencias:
- Basu, S., Pollack, R., Roy, M.-F., On the combinatorial and algebraic complexity of quantifier elimination (1996) J. ACM, 43, pp. 1002-1045
- Basu, S., Pollack, R., Roy, M.-F., Algorithms in Real Algebraic Geometry (2006) Algorithms Comput. Math., 10. , second edition Springer-Verlag Berlin
- Basu, S., Pollack, R., Roy, M.-F., Algorithms in Real Algebraic Geometry (2006) Algorithms Comput. Math., 10. , https://perso.univ-rennes1.fr/marie-francoise.roy/bpr-ed2-posted3.html, New online version available at
- Ben-Or, M., Kozen, D., Reif, J., The complexity of elementary algebra and geometry (1986) J. Comput. Syst. Sci., 18, pp. 251-264
- Berkowitz, S., On computing the determinant in small parallel time using a small number of processors (1984) Inform. Process. Lett., 18, pp. 147-150
- Canny, J., Improved algorithms for sign determination and existential quantifier elimination (1993) Comput. J., 36 (5), pp. 409-418
- https://coq.inria.fr/; Cohen, P.J., Decision procedures for real and p-adic fields (1969) Comm. Pure Appl. Math., 22, pp. 131-151
- Cohen, C., Mahboubi, A., Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination (2012) Log. Methods Comput. Sci., 8 (1:02)
- Collins, G., Quantifier Elimination for real closed fields by cylindric algebraic decomposition (1975) Second GI Conference on Automata Theory and Formal Languages, Lecture Notes in Comput. Sci., 33, pp. 134-183. , Springer-Verlag Berlin
- Coste, M., Roy, M.-F., Thom's lemma, the coding of real algebraic numbers and the computation of the topology of semi-algebraic sets (1988) J. Symbolic Comput., pp. 121-129
- Cox, D., Little, J., O'Shea, D., Ideals, Varieties, and Algorithms. An Introduction to Computational Algebraic Geometry and Commutative Algebra (2007) Undergrad. Texts Math., , third edition Springer New York
- Davenport, J.H., Heintz, J., Real quantifier elimination is doubly exponential (1988) J. Symbolic Comput., 5, pp. 29-35
- Grigoriev, D., Complexity of deciding Tarski algebra (1988) J. Symbolic Comput., 5, pp. 65-108
- Grigoriev, D., Vorobjov, N., Solving systems of polynomial inequalities in subexponential time (1988) J. Symbolic Comput., 5, pp. 37-64
- Hörmander, L., The Analysis of Linear Partial Differential Operators (1983), pp. 364-367. , Springer Berlin, Heidelberg, New-York; Lojasiewicz, S., Ensembles Semi-Analytiques (1965), Institut des Hautes Etudes Scientifiques; Lombardi, H., Perrucci, D., Roy, M.-F., An elementary recursive bound for effective Positivstellensatz and Hilbert 17-th problem (2014), Manuscript; Monk, L.G., Elementary-Recursive Decision Procedures (1975), PhD thesis UC Berkeley; Renegar, J., On the computational complexity and geometry of the first-order theory of the reals. I–III (1992) J. Symbolic Comput., 13, pp. 255-352
- Seidenberg, A., A new decision method for elementary algebra (1954) Ann. of Math., 60, pp. 365-374
- Tarski, A., A Decision Method for Elementary Algebra and Geometry (1951), second edition University of California Press Berkeley and Los Angeles, CA
Citas:
---------- APA ----------
Perrucci, D. & Roy, M.-F.
(2017)
. Elementary recursive quantifier elimination based on Thom encoding and sign determination. Annals of Pure and Applied Logic, 168(8), 1588-1604.
http://dx.doi.org/10.1016/j.apal.2017.03.001---------- CHICAGO ----------
Perrucci, D., Roy, M.-F.
"Elementary recursive quantifier elimination based on Thom encoding and sign determination"
. Annals of Pure and Applied Logic 168, no. 8
(2017) : 1588-1604.
http://dx.doi.org/10.1016/j.apal.2017.03.001---------- MLA ----------
Perrucci, D., Roy, M.-F.
"Elementary recursive quantifier elimination based on Thom encoding and sign determination"
. Annals of Pure and Applied Logic, vol. 168, no. 8, 2017, pp. 1588-1604.
http://dx.doi.org/10.1016/j.apal.2017.03.001---------- VANCOUVER ----------
Perrucci, D., Roy, M.-F. Elementary recursive quantifier elimination based on Thom encoding and sign determination. Ann. Pure Appl. Logic. 2017;168(8):1588-1604.
http://dx.doi.org/10.1016/j.apal.2017.03.001