### Abstract

This formalization is concerned with the theory of Gröbner bases in (commutative) multivariate polynomial rings over fields, originally developed by Buchberger in his 1965 PhD thesis. Apart from the statement and proof of the main theorem of the theory, the formalization also implements Buchberger's algorithm for actually computing Gröbner bases as a tail-recursive function, thus allowing to effectively decide ideal membership in finitely generated polynomial ideals. Furthermore, all functions can be executed on a concrete representation of multivariate polynomials as association lists.

### License

BSD License

### History

April 18, 2019
  Specialized Gröbner bases to less abstract representation of polynomials, where power-products are represented as polynomial mappings.

### Topics

- Mathematics/Algebra
- Computer science/Algorithms/Mathematical

### Session Groebner_Bases

- General
- Confluence
- Reduction
- Groebner_Bases
- Algorithm_Schema
- Buchberger
- Benchmarks
- Algorithm_Schema_Impl
- Code_Target_Rat
- Buchberger_Examples
- More_MPoly_Type_Class
- Auto_Reduction
- Reduced_GB
- Reduced_GB_Examples
- Macaulay_Matrix
- F4
- F4_Examples
- Syzygy
- Syzygy_Examples
- Groebner_PM

### Depends on

- Deriving class instances for datatypes
- Matrices, Jordan Normal Forms, and Spectral Radius Theory
- Executable Multivariate Polynomials

### Used by

- Fisher’s Inequality: Linear Algebraic Proof Techniques for Combinatorics
- Hilbert’s Nullstellensatz
- Gröbner Bases, Macaulay Matrices and Dubé’s Degree Bounds
- Signature-Based Gröbner Basis Algorithms

### Auto-related entries

- Gröbner Bases, Macaulay Matrices and Dubé’s Degree Bounds
- Factorization of Polynomials with Algebraic Coefficients
- Expressiveness of Deep Learning

## Cite

×

Groebner_Bases-AFP

    @article{Groebner_Bases-AFP,
      author  = {Fabian Immler and Alexander Maletzky},
      title   = {Gröbner Bases Theory},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/Groebner_Bases.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 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- May 2, 2016 : Isabelle2016