Journal of the Association for Computing Machinery, Vol. 43, No. 6, November 1996, pp. 1002–1045.

On the Combinatorial and Algebraic Complexity of Quantifier Elimination

SAUGATA BASU

RICHARD POLLACK

AND

MARIE-FRANÇOISE ROY

Abstract. In this paper, a new algorithm for performing quantifier elimination from first order formulas over real closed fields is given. This algorithm improves the complexity of the asymptotically fastest algorithm for this problem, known to this date. A new feature of this algorithm is that the rule of the algebraic part (the dependence on the degrees of the input polynomials) and the combinatorial part (the dependence on the number of the polynomials) are separated. Another new feature is that the degrees of the polynomials in the equivalent quantifier-free formula that is output, are independent of the number of input polynomials. As special cases of this algorithm, new and improved algorithms for deciding a sentence in the first order theory over real closed fields, and also for solving the existential problem in the first order theory over real closed fields, are obtained.

Categories and Subject Descriptors. F.4.3 [Mathematical Logic and Formal Languages]: Formal Languages—decision problems

General Terms. Algorithms, Theory

Additional Key words and Phrases. Quantifier elimination, real closed fields, Tarski-Seidenberg principle

Copyright 1996 by ACM, Inc. Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or direct commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications Dept, ACM Inc., fax +1 (212) 869-0481, or permissions@acm.org.