|Title||Speeding-up 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 CAD-based 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 slow-down. 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.
|Address||Johannes Kepler University, Linz, Austria|
Johannes Kepler University Linz|
RISC (Research Institute for Symbolic Computation)|