On the computational complexity and geometry of the first-order theory of the reals. II: The general decision problem. Preliminaries for quantifier elimination (Q1185457)

From MaRDI portal
scientific article
Language Label Description Also known as
English
On the computational complexity and geometry of the first-order theory of the reals. II: The general decision problem. Preliminaries for quantifier elimination
scientific article

    Statements

    On the computational complexity and geometry of the first-order theory of the reals. II: The general decision problem. Preliminaries for quantifier elimination (English)
    0 references
    0 references
    28 June 1992
    0 references
    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.
    0 references
    decision problem for elementary algebra
    0 references
    0 references

    Identifiers