Home | Quick Search | Advanced Search | Bibliography submission | Bibliography submission using bibtex | Bibliography submission using bibtex file | Links | Help | Internal


TitleSpeeding-up Quantifier Elimination by Gröbner Bases
Author(s) Bruno Buchberger, Hoon Hong
TypeTechnical Report, Misc
AbstractIn 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.
AddressJohannes Kepler University, Linz, Austria
Translation No
Refereed No
Organization Johannes Kepler University Linz
Institution RISC (Research Institute for Symbolic Computation)