Quantoren-Elimination über $\mathbb {R}$

• Sturmsche Ketten verallgemeinern für Polynome in mehreren Variablen
• Variablen der Reihe nach entfernen
• Realisierung durch
  • Tarski (1930): Laufzeit exp(exp(...(| V|)...))
  • Collins (1975): QEPCAD (cyclindrical algebraic decomposition)

    Laufzeit exp(exp(| V|))

implementiert in modernen Computeralgebra-Systemen, vgl.http://www.singular.uni-kl.de/Manual/3-1-3/sing_1815.htm