Details:
Title  Speedingup Quantifier Elimination by Gröbner Bases  Author(s)  Bruno Buchberger, Hoon Hong  Type  Technical Report, Misc  Abstract  In this paper we investigate the possibility of using the first author's Gröbner bases algorithm for speeding up the CADbased quantifier
elimination algorithm (QE) which was discovered by Collins and improved by the second author. In particular, we use the Gröbner bases algorithm
to preprocess input formulas of QE into equivalent, but often "triangularized", formulas. Then the improved QE algorithm utilizes such
structure to complete quantifier elimination with partially built CAD's.
Preliminary experiments show that this method often gives a significant speedup, though sometimes it results in a slowdown. Further study is needed for explaining when and why the use of Gröbner bases is not helpful. Then based on the resulting understanding, we could be able to adapt the Gröbner bases algorithm to our use.  Length  20 
File 
 Language  English  Number  9106  Address  Johannes Kepler University, Linz, Austria  Year  1991  Month  February  Edition  0  Translation 
No  Refereed 
No  Organization 
Johannes Kepler University Linz  Institution 
RISC (Research Institute for Symbolic Computation) 
