The Geometry of Cylindrical Algebraic Decomposition

The decision problem of the first order theory over the reals is a fundamental problem in symbolic computation. Because many problems emerging from other areas of science and engineering can be directly expressed by a decision problem over the reals, there are more and more interests in developing efficient algorithms for the decision problem. For example, the non-linear real arithmetic (NRA) theory in satisfiability modulo theories (SMT) is a special case of the real decision problem, where all variables are existentially quantified. And there are applications in Robotics, Biology and Economics. More and more new applications are discovered all the time. Besides, the real decision problem is related to many different branches of mathematics, such as logic, geometry, algebra and computation. Therefore, the decision problem over the reals is interesting to both the mathematics community and researchers from other science areas.