License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.10161.3
URN: urn:nbn:de:0030-drops-27345
URL: http://dagstuhl.sunsite.rwth-aachen.de/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:
10161.PassmoreGrant.Paper.2734.pdf (0.4 MB)

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:DagSemProc.10161.3,
  author =	{Passmore, Grant Olney and de Moura, Leonardo and Jackson, Paul B.},
  title =	{{Gr\"{o}bner Basis Construction Algorithms Based on Theorem Proving Saturation Loops}},
  booktitle =	{Decision Procedures in Software, Hardware and Bioware},
  pages =	{1--17},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10161},
  editor =	{Nikolaj Bjorner and Robert Nieuwenhuis and Helmut Veith and Andrei Voronkov},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2010/2734},
  URN =		{urn:nbn:de:0030-drops-27345},
  doi =		{10.4230/DagSemProc.10161.3},
  annote =	{Keywords: Groebner bases, ideal theory, automated theorem proving, SMT solvers}
}

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

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI