Complexity of Tarski- Seidenberg’s principle. (Complexité du principe de Tarski-Seidenberg.) (French) Zbl 0704.03013

The authors prove the following theorem. Let \(\phi\) be a first order formula of the language of ordered fields in prenex form with m alternations of quantifiers defined by s polynomials in n variables such that the sum of their total degrees is bounded by d. They describe an algorithm computing a quantifier free formula equivalent (in any real closed field) to \(\phi\) with parallel complexity \(n^{O(m)}\log d^{O(1)}\) and sequential complexity \(n^{n^{O(m)}}\).


03C10 Quantifier elimination, model completeness, and related topics
14G25 Global ground fields in algebraic geometry
68Q25 Analysis of algorithms and problem complexity
03C60 Model-theoretic algebra
12L12 Model theory of fields