2026-07-22T06:26:06Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:2734 2024-03-06T11:09:17Z ddc:004 open_access

Gröbner Basis Construction Algorithms Based on Theorem Proving Saturation Loops Passmore, Grant Olney de Moura, Leonardo Jackson, Paul B. Groebner bases ideal theory automated theorem proving SMT solvers 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Grant Olney Passmore and Leonardo de Moura and Paul B. Jackson 2010 Is Part Of Dagstuhl Seminar Proceedings, Volume 10161, Decision Procedures in Software, Hardware and Bioware (2010) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DagSemProc.10161.3 urn:nbn:de:0030-drops-27345 https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10161.3 eng https://creativecommons.org/licenses/by/4.0/legalcode