License
When quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-27345
URL: http://drops.dagstuhl.de/opus/volltexte/2010/2734/
Go to the corresponding Portal

Passmore, Grant Olney ; de Moura, Leonardo ; Jackson, Paul B.

Gröbner Basis Construction Algorithms Based on Theorem Proving Saturation Loops

pdf-format:
Document 1.pdf (446 KB)

Abstract

We present novel Gr"obner 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.

BibTeX - Entry

@InProceedings{passmore_et_al:DSP:2010:2734,
  author =	{Grant Olney Passmore and Leonardo de Moura and Paul B. Jackson},
  title =	{Gr{\"o}bner Basis Construction Algorithms Based on Theorem Proving Saturation Loops},
  booktitle =	{Decision Procedures in Software, Hardware and Bioware},
  year =	{2010},
  editor =	{Nikolaj Bjorner and Robert Nieuwenhuis and Helmut Veith and Andrei Voronkov},
  number =	{10161},
  series =	{Dagstuhl Seminar Proceedings},
  ISSN =	{1862-4405},
  publisher =	{Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2010/2734},
  annote =	{Keywords: Groebner bases, ideal theory, automated theorem proving, SMT solvers}
}

Keywords: Groebner bases, ideal theory, automated theorem proving, SMT solvers
Seminar: 10161 - Decision Procedures in Software, Hardware and Bioware
Issue Date: 2010
Date of publication: 25.08.2010

DROPS-Home | Fulltext Search | Imprint Published by LZI