×

zbMATH — the first resource for mathematics

On the computational complexity and geometry of the first-order theory of the reals. II: The general decision problem. Preliminaries for quantifier elimination. (English) Zbl 0763.68043
This second paper in a series is devoted to the complexity of the decision problem for “elementary algebra”. See the above review of the first paper for the general framework, results, references and notations. The algorithm is first explained in the case of one alternation of quantifiers, when there are two blocks \(x^{[1]}\) and \(x^{[2]}\) of variables. The construction \({\mathcal R}\) mentioned above, which allows to reduce to a univariate problem with the help of \(u\)-resultant, is sufficiently uniform to be performed on \(x^{[2]}\) with parameters \(x^{[1]}\), and so one gets a list of polynomials in \(x^{[1]}\) and one variable \(t\). The projection which forgets \(t\) is dealt with the ideas of Collins’ algorithm of cylindrical algebraic decomposition, to get a list \(h\) of polynomials in \(x^{[1]}\). The algorithm of the first paper furnishes at least one point for each member of the connected sign partition of \(h\). These points are coded using Thom’s lemma, and this is sufficient to perform the calculations in the fibers above these points needed for decision. The general case for decision is then explained, and some preparations for the quantifier elimination problem (the subject of the third paper) are made.
This series of papers contains the best general results (up to now) on the complexity of decision and quantifier elimination for the reals. It has the advantage of being self contained. Perhaps due to this, and also to the many technicalities involved, the papers are not very easy to read. For instance, the point which makes the difference in the exponent of the bound (each block of variables contributes only according to its own length), does not appear clearly. So it is advisable to read the author’s “synopsis” [Discrete and computational geometry, Proc. DIMACS Spec. Year Workshops 1989-90, DIMACS, Ser. Discret. Math. Theor. Comput. Sci. 6, 287-308 (1991; Zbl 0741.03004)], and to follow the reading guide given in the introduction.
Reviewer: M.Coste (Rennes)

MSC:
68Q25 Analysis of algorithms and problem complexity
14P10 Semialgebraic sets and related spaces
03B25 Decidability of theories and sets of sentences
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Collins, G.E., Quantifier elimination for real closed fields by cylindrical algebraic decomposition, Second GI conference on automata theory and formal languages, lecture notes in computer science, 33, 134-183, (1975)
[2] Coste, M.; Roy, M.F., Thorn’s lemma, the coding of real algebraic numbers and the computation of the topology of semi-algebraic sets, J. symbolic computation, 5, 121-129, (1988) · Zbl 0689.14006
[3] Csanky, L., Fast parallel matrix inversion algorithms, SIAM journal on computing, 5, 618-623, (1976) · Zbl 0353.68063
[4] Fitchas, N.; Galligo, A.; Morgenstern, J., Algorithmes rapides en séquential et en parallele pour l’élimination de quantificateurs en géométrie élémentaire, (), VII · Zbl 0704.03014
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.