Die reelle Algebra beschäftigt sich mit der Struktur von Lösungen von Polynomgleichungs- und Ungleichungssystemen im Reellen oder allgemeiner in reell-abgeschlossenen geordneten Körpern. Die Eigenschaften dieser semi-algebraischen Mengen weichen erheblich von denen komplexer Varietäten ab. Ein grundlegendes Werkzeug zur algorithmischen Untersuchung solcher Mengen sind Quantoreneliminationsverfahren, d.h. die Berechnung von Projektionen solcher Mengen auf niedriger-dimensionale Teilräume. Seit A. Tarski in den 30er Jahren sind eine Fülle verschiedener solcher Verfahren angegeben worden, von denen jedoch nur ein Typ, die zylindrisch-algebraische Zellenzerlegung (Collins-Hong) bisher mit Erfolg implementiert wurde. Vor kurzem wurde nun eine überraschende Erweiterung des algorithmischen Zählens reeller Nullstellen von univariaten (Sturm-Hermite-Sylvester) auf multivariate nulldimensionale Ideale gefunden (Becker-Wörmann, Pedersen-Roy-Szpirglas).
Zusammen mit der Konstruktion umfassender Gröbnerbasen bietet dieses Verfahren einen ganz neuen, vielversprechenden Zugang zu dem Quantoreneliminationsproblem []. Eine Implementierung dieses Verfahrens hat begonnen; Ziel sind Optimierungen, die zumindest in Teilbereichen dem Collins-Hong Verfahren erheblich überlegen sind.
Für ein Teilproblem (lineare Quantorenelimination) wurde in
[][] ein gutes Verfahren angegeben, das sich schon an
Problemen interessanter Größe bewährt hat. Ein entsprechendes
Verfahren für ganzzahlige Probleme wurde in [] angegeben, am
Lehrstuhl implementiert und soll weiter optimiert werden. Für
-adische Körper wurden entsprechende Algorithmen in []
angegeben; eine Implementierung ist geplant.