ON THE COMPLEXITY OF QUANTIFIER ELIMINATION - THE STRUCTURAL APPROACH

The aim of this paper is to survey certain theoretical aspects of the complexity of quantifier elimination in the elementary theory of the r eal numbers with real constants, and to present some new results on th e subject. We use the new model of computation introduced by L. Blum, M. Shub and S. Smale that accepts as inputs vectors of real numbers an d allows the transfer of the stuctural approach to computability and c omplexity for computations with real numbers. More concretely, we give a proof of the existence of NP(R)-complete problems. Also, we introdu ce a new complexity class PAT(R) which describes the complexity of the decision of quantified formulae and, in order to study its relationsh ips with the already existing complexity classes, a model for parallel computations is also introduced. Using the classes resulting by bound ing resources in this parallel model, some separation results are fina lly obtained. In particular, we show that the polynomial hierarchy ove r the reals is strictly contained in PAT(R).