Real quantifier elimination is doubly exponential

Abstract

We show that quantifier elimination over real closed fields can require doubly exponential space (and hence time). This is done by explicitly constructing a sequence of expressions whose length is linear in the number of quantifiers, but whose quantifier-free expression has length doubly exponential in the number of quantifiers. The results can be applied to cylindrical algebraic decomposition, showing that this can be doubly exponential. The double exponents of our lower bounds are about one fifth of the double exponents of the best-known upper bounds. © 1988, Academic Press Limited. All rights reserved.