We consider existential problems over the reals. Extended quantifier elimination generalizes the concept of regular quantifier elimination by providing in addition answers, which are descriptions of possible assignments for the quantified variables. Implementations of extended quantifier elimination for the quadratic case via virtual substitution have been successfully applied to various problems in science and engineering. So far, the answers produced by these implementations included infinitesimal and infinite numbers, which are hard to interpret in practice. We introduce here a post-processing procedure to convert, for fixed parameters, all answers into standard real numbers. The relevance of our procedure is demonstrated by application of our implementation to various examples from the literature, where it significantly improves the quality of the results.

We present a method based on extended linear real quantifier elimination for multiple object semilinear motion planning, i.e. finding collision-free trajectories for several robots in a time dependent environment. For practical applicability the method is limited to polygonal objects and linear trajectories. It can, however, deal with situations involving even non-convex objects.

We describe an algorithm for quantifier elimination over di fferentially closed fields and its implementation within the computer log ic packageREDLOG of the computer algebra system REDUCE. We give various application examples, which on the one hand demonstrate the applicabili ty of our software to non-trivial problems, and on the other hand give a goo d impression of the possible range of applications of our work. Essential ly, our elimination technique dates back to Seidenberg. It has been made m uch ore explicit on the basis of the common axioms for di fferentially closed fields in lectures on di fferential algebra by Weispfenning. In this explicit form, which we use and describe here, it had remained unpublished s o far. dolzmann@uni-passau.de , http://www.fmi.uni-passau.de/ ̃dolzmann/ sturm@uni-passau.de , http://www.fmi.uni-passau.de/ ̃sturm/

We introduce an efficient algorithm for determining a suitable projection order for performing cylindrical algebraic decomposition. Our algorithm is motivated by a statistical analysis of comprehensive test set computations. This analysis introduces several measures on both the projection sets and the entire computation, which turn out to be highly correlated. The statistical data also shows that the orders generated by our algorithm are significantly close to optimal.

We present a new method for generic quantifier elimination that uses an extension of Hermitian quantifier elimination. By means of sample computations we show that this generic Hermitian quantifier elimination is, for instance, an important method for automated theorem proving in geometry.

We describe an algorithm for quantifier elimination over differentially closed fields and its implementation within the computer logic package redlog of the computer algebra system reduce. We give various application examples, which on the one hand demonstrate the applicability of our software to non-trivial problems, and on the other hand give a good impression of the possible range of applications of our work. Essentially, our elimination technique dates back to Seidenberg. It has been made much more explicit on the basis of the common axioms for differentially closed fields in lectures on differential algebra by Weispfenning. In this explicit form, which we use and describe here, it had remained unpublished so far.

We describe an algorithm for quantifier elimination over dierentially closed fields and its implementation within the computer logic package redlog of the computer algebra system reduce. We give various application examples, which on the one hand demon- strate the applicability of our software to non-trivial problems, and on the other hand give a good impression of the possible range of applications of our work. Essentially, our elim- ination technique dates back to Seidenberg. It has been made much more explicit on the basis of the common axioms for dierentially closed fields in lectures on dierential algebra by Weispfenning. In this explicit form, which we use and describe here, it had remained unpublished so far.

yields {x, y} as reduced Grobner basis. This is, however, not correct under the specialization a = 0. The reduced Grobner basis would then be {x + y}. Taking these results together, we obtain C = {x + y, ax, ay}, which is correct wrt. all specializations for a including zero specializations. We call this set C a comprehensive Grobner basis (cgb). The notion of a cgb and a corresponding algorithm has been introduced bei Weispfenning [?]. This algorithm works by performing case distinctions wrt. parametric coefficient polynomials in order to find out what the head monomials are under all possible specializations. It does thus not only determine a cgb, but even classifies the contained polynomials wrt. the specializations they

redlog is a system for computing with first-order logic and propositional logic with quantification. It is tightly integrated into the computer algebra system reduce. Assuming a broad audience, we motivate the use of first-order logic to model problems. Then, by employing quantifier elimination methods, simplification techniques and normal form computations, highly non-trivial problems can be solved. We give an overview of redlog's capabilities, features and applications. Finally we explain how computer algebra benefits from computer logic and vice versa.

Based on an extended quantifier elimination procedure for discretely valued fields, we devise algorithms for solving multivariate systems of linear congruences over the integers. This includes determining integer solutions for sets of moduli which are all power of a fixed prime, uniform p-adic integer solutions for parametric prime power moduli, lifting strategies for these uniform p-adic solutions for given primes, and simultaneous lifting strategies for finite sets of primes. The method is finally extended to arbitrary moduli.

Many problems arising in real geometry can be formulated as first-order formulas. Thus quantifier elimination can be used to solve these problems. In this note, we discuss the applicability of implemented quantifier elimination algorithms for solving geometrical problems. In particular, we demonstrate how the tools of redlog can be applied to solve a real implicitization problem, namely the Enneper surface.

We introduce local quantifier elimination as a new variant of real quantifier elimination. Given a first-order formula and a real point we compute a quantifier-free formula which is not only for the given point equivalent to the input formula but also for all points in a semi-algebraic set containing the specified point. The description of this semi-algebraic set is explicitly computed in the form of a conjunction of atomic formulas. Local quantifier elimination is in its application area superior to both regular and generic quantifier elimination due to faster running times and shorter results.

Eines der bedeutendsten Verfahren zur reellen Quantorenelimination ist die Quantorenelimination mittels virtueller Substitution, die von Weispfenning 1988 eingefuhrt wurde. In der vorliegenden Arbeit werden zahlreiche algorithmische Strategien zur Optimierung dieses Verfahrens prasentiert. Optimierungsziele der Arbeit waren dabei die tatsachliche Laufzeit der Implementierung des Algorithmus sowie die Grose der Ausgabeformel. Zur Optimierung werden dabei die Simplifikation von Formeln erster Stufe, die Reduktion der Grose der Eliminationsmenge sowie das Condensing, ein Ersatz fur die virtuelle Substitution, untersucht. Lokale Quantorenelimination berechnet Formeln, die nur in der Nahe eines gegebenen Punktes aquivalent zur Eingabeformel ist. Diese Einschrankung erlaubt es, das Verfahren weiter zu verbessern. Als Anwendung des Eliminationsverfahren diskutieren wir abschliesend, wie man eine grose Klasse von Schedulingproblemen mittels reeller Quantorenelimination losen kann. In diesem Fall benutzen wir die spezielle Struktur der Eingabeformel und zusatzliche Informationen uber das Schedulingproblem, um die Quantorenelimination mittels virtueller Substitution problemspezifisch zu optimieren.

IntroductionConsider the ideal basis F ={ax,x + y}. Treating a as a parameter, the callingsequencetorder({x,y},lex)$groebner{a*x,x+y};{x,y}yields{x,y} as reduced Grobner basis. This is, however, not correct under thespecialization a = 0. The reduced Grobner basis would then be{x+ y}. Takingthese results together, we obtain C ={x+ y, ax, ay}, which is correct wrt. all specializationsfor a including zero specializations. We call this set C a comprehensiveGrobner...