!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Groebner_Bases
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Groebner_Bases |
AFP entry Groebner_Bases |
Statements
Fabian Immler
0 references
Alexander Maletzky
0 references
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.
0 references
0 references
2 May 2016
0 references
Gröbner Bases Theory (English)
0 references
