### Abstract

This article formalizes signature-based algorithms for computing Gröbner bases. Such algorithms are, in general, superior to other algorithms in terms of efficiency, and have not been formalized in any proof assistant so far. The present development is both generic, in the sense that most known variants of signature-based algorithms are covered by it, and effectively executable on concrete input thanks to Isabelle's code generator. Sample computations of benchmark problems show that the verified implementation of signature-based algorithms indeed outperforms the existing implementation of Buchberger's algorithm in Isabelle/HOL.

Besides total correctness of the algorithms, the article also proves that under certain conditions they a-priori detect and avoid all useless zero-reductions, and always return 'minimal' (in some sense) Gröbner bases if an input parameter is chosen in the right way.

The formalization follows the recent survey article by Eder and Faugère.

### License

BSD License

### Topics

- Mathematics/Algebra
- Computer science/Algorithms/Mathematical

### Session Signature_Groebner

- Prelims
- More_MPoly
- Signature_Groebner
- Signature_Examples

### Depends on

- Gröbner Bases Theory

### Auto-related entries

- Factorization of Polynomials with Algebraic Coefficients
- Putting the `K' into Bird’s derivation of Knuth-Morris-Pratt string matching
- Weight-Balanced Trees
- Büchi Complementation
- Formalizing the Edmonds-Karp Algorithm

## Cite

×

Signature_Groebner-AFP

    @article{Signature_Groebner-AFP,
      author  = {Alexander Maletzky},
      title   = {Signature-Based Gröbner Basis Algorithms},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2018},
      note    = {\url{https://isa-afp.org/entries/Signature_Groebner.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Sep 20, 2018 : Isabelle2018