Real Quantifier Elimination by Computation of Comprehensive Gröbner Systems

A real quantifier elimination method based on the theory of real root counting and the computation of comprehensive Gröbner systems introduced by V. Weispfenning is studied in more detail. We introduce a simpler and more intuitive algorithm which is shown to be an improvement of the original algorithm. Our algorithm is implemented on the computer algebra system Maple using a recent algorithm to compute comprehensive Gröbner systems together with several simplification techniques. According to our computation experiments, our program is superior to other existing implementations for many examples which contain many equalities.