Algorithms for computing with real algebraic numbers (in particular, (i) computing the sign of an algebraic real A presented, for instance, as a pair of a minimal polynomial P $\in \mathbb{Z}[x]$ for A and an interval with rational endpoints containing A and no other real roots of P, and (ii) computing the sign of a polynomial evaluated at algebraic real numbers presented in form (i)) are critical components of some modern quantifier elimination based decision procedures for real algebra such as cylindrical algebraic decomposition. These procedures are used in a number of areas: formal verification of hardware, software and bioware (including control systems and other `hybrid' systems with both discrete and continuous dynamics), robot motion planning, correctly displaying algebraic curves on computers, testing the stability of initial and initial-boundary value problems, and formalised mathematics.
--
[Some references on cylindrical algebraic decomposition (CAD)]
Caviness, B. F. and Johnson, J. R. (Eds.). Quantifier Elimination and Cylindrical Algebraic Decomposition. New York: Springer-Verlag, 1998. (The `CAD bible' - Collins's festschrift.)
Collins, G. E. "Quantifier Elimination for the Elementary Theory of Real Closed Fields by Cylindrical Algebraic Decomposition." Lect. Notes Comput. Sci. 33, 134-183, 1975.
Collins, G. E. "Quantifier Elimination by Cylindrical Algebraic Decomposition--Twenty Years of Progress." In Quantifier Elimination and Cylindrical Algebraic Decomposition (Ed. B. F. Caviness and J. R. Johnson). New York: Springer-Verlag, pp. 8-23, 1998.
--
[Some references on applications of CAD: there are many, I only post a few]
(robot motion planning)
S. Lindemann and S. LaValle. "Computing Smooth Feedback Plans Over Cylindrical Algebraic Decompositions." In Proceedings of Robotics: Science and Systems, 2006.
(formal verification of systems)
M. Adlaide and O. Roux. "Using Cylindrical Algebraic Decomposition for the Analysis of Slope Parametric Hybrid Automata." In Proceedings of the 6th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, 2000.
(formalised mathematics)
A. Mahboubi, "Programming and certifying the CAD algorithm inside the Coq system." In Mathematics: Algorithms, Proofs. Volume 05021 of Dagstuhl Seminar Proceedings, Schloss Dagstuhl, 2005.
(display of algebraic curves)
D.S. Arnon. "Topologically reliable display of algebraic curves." SIGGRAPH Comput. Graph. 17, 3 (Jul. 1983), 219-227.
--
Also, many open problems in metric geometry actually fall within the theory of real closed fields (RCF), and thus can in principle be decided by the CAD algorithm. The issue is one of complexity. Due to Davenport-HeinzDavenport-Heintz, it is known that real quantifier elimination is inherently doubly exponential in the dimension (number of variables) of the input formula. Similarly, due to Ben-Or and KozenThus, it is known that the decision problem for the existential fragment of the theory case of real closed fields is PSPACE-complete. ThusRCF, decidable in principle does not mean decidable in practice. Nevertheless, it is a fascinating state of affairs. Complexity aside, here are some examples:
All kissing problems for n-dimensional hyperspheres are in principle decidable by CAD and other real algebra decision methods.
Due to L. Fejes Toth, Kepler's conjecture is known to be equivalent to a single RCF sentence, and thus could be decided by CAD as well. In the formalisation of his proof of the Kepler conjecture, Thomas Hales has isolated a large collection of RCF sentences which appear as lemmata in his proof and which he believes should be amenable to specialised RCF decision methods. See T. Hales's ``A Collection of Problems in Elementary Geometry'' ( flyspeck.googlecode.com/files/collection_geom.pdf ).
