Algorithmic strategies for applicable real quantifier elimination

One of the most important algorithms for real quantifier elimination is the quantifier elimination by virtual substitution introduced by Weispfenning in 1988. In this thesis we present numerous algorithmic approaches for optimizing this quantifier elimination algorithm. Optimization goals are the actual running time of the implementation of the algorithm and the size of the output formula. Strategies for obtaining these goals include simplification of first-order formulas,reduction of the size of the computed elimination set, and condensing a new replacement for the virtual substitution. Local quantifier elimination computes formulas that are equivalent to the input formula only nearby a given point. We can make use of this restriction for further optimizing the quantifier elimination by virtual substitution. Finally we discuss how to solve a large class of scheduling problems by real quantifier elimination. To optimize our algorithm for solving scheduling problems we make use of the special form of the input formula and of additional information given by the description of the scheduling problemEines der bedeutendsten Verfahren zur reellen Quantorenelimination ist die Quantorenelimination mittels virtueller Substitution, die von Weispfenning 1988 eingeführt wurde. In der vorliegenden Arbeit werden zahlreiche algorithmische Strategien zur Optimierung dieses Verfahrens präsentiert. Optimierungsziele der Arbeit waren dabei die tatsächliche Laufzeit der Implementierung des Algorithmus sowie die Größe der Ausgabeformel. Zur Optimierung werden dabei die Simplifikation vonFormeln erster Stufe, die Reduktion der Größe der Eliminationsmenge sowie das Condensing, ein Ersatz für die virtuelle Substitution,untersucht. Lokale Quantorenelimination berechnet Formeln, die nur inder Nähe eines gegebenen Punktes äquivalent zur Eingabeformel ist. Diese Einschränkung erlaubt es, das Verfahren weiter zu verbessern.Als Anwendung des Eliminationsverfahren diskutieren wir abschließend, wie man eine große Klasse von Schedulingproblemen mittels reeller Quantorenelimination lösen kann. In diesem Fall benutzen wir die spezielle Struktur der Eingabeformel und zusätzliche Informationen über das Schedulingproblem, um die Quantorenelimination mittels virtueller Substitution problemspezifisch zu optimieren