@inproceedings{3a169d3f2f4e49f099a2bfd2163d4c20,
title = "Gr{\"o}bner Basis Construction Algorithms Based on Theorem Proving Saturation Loops",
abstract = "We present novel Gr{\"o}bner basis algorithms based on saturation loops used by modern superposition theorem provers. We illustrate the practical value of the algorithms through an experimental implementation within the Z3 SMT solver. ",
author = "Passmore, {Grant Olney} and Moura, {Leonardo de} and Jackson, {Paul B.}",
year = "2010",
language = "English",
series = "Dagstuhl Seminar Proceedings",
publisher = "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany",
pages = "1--17",
editor = "Nikolaj Bjorner and Robert Nieuwenhuis and Helmut Veith and Andrei Voronkov",
booktitle = "Decision Procedures in Software, Hardware and Bioware",
}