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

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



PDF
Thumbnail PDF

File

DagSemProc.10161.3.pdf
  • Filesize: 446 kB
  • 17 pages

Document Identifiers

Author Details

Grant Olney Passmore
Leonardo de Moura
Paul B. Jackson

Cite As Get BibTex

Grant Olney Passmore, Leonardo de Moura, and Paul B. Jackson. Gröbner Basis Construction Algorithms Based on Theorem Proving Saturation Loops. In Decision Procedures in Software, Hardware and Bioware. Dagstuhl Seminar Proceedings, Volume 10161, pp. 1-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010) https://doi.org/10.4230/DagSemProc.10161.3

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.

Subject Classification

Keywords
  • Groebner bases
  • ideal theory
  • automated theorem proving
  • SMT solvers

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail