Artículo

Estamos trabajando para incorporar este artículo al repositorio
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

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