|
|
|
Tarski's theorem states that the first-order theory of the Field of Real Numbers is Decidable. However, the best-known Algorithm for eliminating Quantifiers is doubly exponential in the number of Quantifier blocks (Heintz et al. 1989).
References
Heintz, J.; Roy, R.-F.; and Solerno, P. ``Complexité du principe de Tarski-Seidenberg.''
C. R. Acad. Sci. Paris Sér. I Math. 309, 825-830, 1989.
Marker, D. ``Model Theory and Exponentiation.'' Not. Amer. Math. Soc. 43, 753-759, 1996.
Tarski, A. ``Sur les ensembles définissables de nombres réels.'' Fund. Math. 17, 210-239, 1931.
Tarski, A. ``A Decision Method for Elementary Algebra and Geometry.'' RAND Corp. monograph, 1948.