Quantifier elimination and cylindrical algebraic decomposition. Proceedings of a symposium, Linz, Austria, October 6--8, 1993 (Q1355986)

The articles of this volume will be reviewed individually. The book contains the contributions of the participants of the symposium on quantifier elemination and cylindrical algebraic decomposition, which was held in Linz (Austria) during October 1993. The Cylindrical Algebraic Decomposition (CAD) is a method of eliminating quantifiers in the language of real arithmetic. This language contains symbols for addition, multiplication and inequality in the reals, together with symbols for 0 and 1. The formulas of the language are built from these symbols, the usual quantifiers -- existential and universal -- and parenthesis; in the usual way one builds `meaningful' formulas in mathematics. Any algorithm for eliminating quantifiers, such as CAD, inputs such a formula and outputs an equivalent formula without quantifiers. It was first demonstrated by Tarski, in 1930, that such an algorithm exists. It is clear that a quantifier-free equivalent of a formula is easy to handle -- algorithmically and mathematically; if the initial formula was a sentence, then the quantifier-free equivalent is a Boolean combination of equations and inequalities among constants (rational numbers) which is either true -- if the sentence was true -- or false. In such a way one can verify or reject algorithmically guessed `possible theorems'. In general the quantifier-free equivalent of a formula reveals the mathematical content of the original formula in a way easily to handle. The main problem with such algorithms is their time complexity. The worst case complexity of the original algorithm of Tarski is given by a stack of exponentials whose size depends on the number of quantifiers. Collins, the inventor of CAD, has given a doubly exponential -- in the number of variables -- time complexity for his algorithm; Davenport, Heintz and recently Weispfenning have given doubly exponential lower bounds, even for simple formulas such as linear ones. The intrinsic hardness of the problem calls for study of the particular types of formulas that arise from each application and the development of `tricks', appropriate for each type. While now there are other methods for quantifier elimination, besides CAD, the latter has a distinct topological character in the sense that intermediate results in a computation often reveal topological properties of the set which is defined by the treated formula. The book is a nearly complete presentation of the history of the development of CAD algorithms and its applications, and is suitable for the beginner as well as the expert. Contents: \textit{B. F. Caviness} and \textit{J. R. Johnson}, ``Introduction'' (pp. 1-7); \textit{G. E. Collins}, ``Quantifier elimination by cylindrical algebraic decomposition -- twenty years of progress'' (pp. 8-23); \textit{A. Tarski}, ``A decision method for elementary algebra and geometry'' (pp. 24-84) [Reprint of the second edition of the monograph (1951; Zbl 0044.25102)]; \textit{G. E. Collins}, ``Quantifier elimination for real closed fields by cylindrical algebraic decomposition'' (pp. 85-121) [Reprint from: Lect. Notes Comput. Sci. 33, 134-183 (1975; Zbl 0318.02051)]; \textit{M. J. Fischer} and \textit{M. O. Rabin}, ``Super-exponential complexity of Presburger arithmetic'' (pp. 122-135) [Reprint from: Complexity of computation, Proc. Symp. Appl. Math. New York City 1973, 27-41 (1974; Zbl 0319.68024)]; \textit{D. S. Arnon}, \textit{G. E. Collins} and \textit{S. McCallum}, ``Cylindrical algebraic decomposition. I. The basic algorithm'' (pp. 136-151) [Reprinted from: SIAM J. Comput. 13, 865-877 (1984; Zbl 0562.14001)]; \textit{D. S. Arnon}, \textit{G. E. Collins} and \textit{S. McCallum}, ``Cylindrical algebraic decomposition. II. An adjacency algorithm for the plane'' (pp. 152-165) [Reprinted from: SIAM J. Comput. 13, 878-889 (1984; Zbl 0562.14001)]; \textit{H. Hong}, ``An improvement of the projection operator in cylindrical algebraic decomposition'' (pp. 166-173) [Reprinted from: S. Watanabe et al. (eds.), Symbolic and algebraic computation, Proc. Int. Symp., 261-264 (ACM Press, 1990)]; \textit{G. E. Collins} and \textit{H. Hong}, ``Partial cylindrical algebraic decomposition for quantifier elimination'' (pp. 174-200) [Reprinted from: J. Symb. Comput. 12, No. 3, 299-328 (1991; Zbl 0754.68063)]; \textit{H. Hong}, ``Simple solution formula construction in cylindrical algebraic decomposition based quantifier elimination'' (pp. 201-219) [Reprinted from: P. S. Wang (ed.), Symbolic and algebraic computation, Proc. Int. Symp., 177-188 (ACM Press, 1992)]; \textit{J. Renegar}, ``Recent progress on the complexity of the decision problem for the reals'' (pp. 220-241) [Reprinted from: DIMACS, Ser. Discrete Math. Theor. Comput. Sci. 6, 287-308 (1991; Zbl 0741.03004)]; \textit{S. McCallum}, ``An improved projection operation for cylindrical algebraic decomposition'' (pp. 242-268); \textit{J. R. Johnson}, ``Algorithms for polynomial real root isolation'' (pp. 269-299); \textit{L. González-Vega}, \textit{T. Recio}, \textit{H. Lombardi} and \textit{M.-F. Roy}, ``Sturm-Habicht sequences, determinants and real roots of univariate polynomials'' (pp. 300-316); \textit{G. Hagel}, ``Characterizations of the Macaulay matrix and their algorithmic impact'' (pp. 317-326); \textit{H. Hong} and \textit{J. R. Sendra}, ``Computation of variant resultants'' (pp. 327-340); \textit{S. Basu}, \textit{R. Pollack} and \textit{M.-F. Roy}, ``A new algorithm to find a point in every cell defined by a family of polynomials'' (pp. 341-350); \textit{D. Richardson}, ``Local theories and cylindrical decomposition'' (pp. 351-364); \textit{L. González-Vega}, ``A combinatorial algorithm solving some quantifier elimination problems'' (pp. 365-375); \textit{V. Weispfenning}, ``A new approach to quantifier elimination for real algebra'' (pp. 376-392). Indexed articles: \textit{Caviness, B. F.; Johnson, J. R.}, Introduction, 1-7 [Zbl 0900.03051] \textit{Collins, George E.}, Quantifier elimination by cylindrical algebraic decomposition -- twenty years of progress, 8-23 [Zbl 0900.03053] \textit{Tarski, Alfred}, A decision method for elementary algebra and geometry, 24-84 [Zbl 0900.03045] \textit{Collins, George E.}, Quantifier elimination for real closed fields by cylindrical algebraic decomposition, 85-121 [Zbl 0900.03055] \textit{Fischer, Michael J.; Rabin, Michael O.}, Super-exponential complexity of Presburger arithmetic, 122-135 [Zbl 0900.03027] \textit{Arnon, Dennis S.; Collins, George E.; McCallum, Scott}, Cylindrical algebraic decomposition. I: The basic algorithm, 136-151 [Zbl 0900.03049] \textit{Arnon, Dennis S.; Collins, George E.; McCallum, Scott}, Cylindrical algebraic decomposition. II: An adjacency algorithm for the plane, 152-165 [Zbl 0900.03050] \textit{Hong, Hoon}, An improvement of the projection operator in cylindrical algebraic decomposition, 166-173 [Zbl 0900.68280] \textit{Collins, George E.; Hong, Hoon}, Partial cylindrical algebraic decomposition for quantifier elimination, 174-200 [Zbl 0900.03052] \textit{Hong, Hoon}, Simple solution formula construction in cylindrical algebraic decomposition based quantifier elimination, 201-219 [Zbl 0900.03054] \textit{Renegar, James}, Recent progress on the complexity of the decision problem for the reals, 220-241 [Zbl 0900.03059] \textit{McCallum, Scott}, An improved projection operation for cylindrical algebraic decomposition, 242-268 [Zbl 0900.68279] \textit{Johnson, J. R.}, Algorithms for polynomial real root isolation, 269-299 [Zbl 0900.12001] \textit{González-Vega, L.; Recio, T.; Lombardi, H.; Roy, M.-F.}, Sturm-Habicht sequences, determinants and real roots of univariate polynomials, 300-316 [Zbl 0900.12002] \textit{Hagel, Georg}, Characterizations of the Macaulay matrix and their algorithmic impact, 317-326 [Zbl 0900.03047] \textit{Hong, Hoon; Sendra, J. Rafael}, Computation of variant resultants, 327-340 [Zbl 0900.03048] \textit{Basu, Saugata; Pollack, Richard; Roy, Marie-Françoise}, A new algorithm to find a point in every cell defined by a family of polynomials, 341-350 [Zbl 0900.68278] \textit{Richardson, Daniel}, Local theories and cylindrical decomposition, 351-364 [Zbl 0900.03057] \textit{González-Vega, Laureano}, A combinatorial algorithm solving some quantifier elimination problems, 365-375 [Zbl 0900.68277] \textit{Weispfenning, V.}, A new approach to quantifier elimination for real algebra, 376-392 [Zbl 0900.03046]