|Keywords||Gröbner bases, Buchberger's algorithm, reduction rings|
|Put online||April 22, 2016|
|Size||43.1 MB (zipped), 760.5 MB (unzipped)|
|Download||Reduction Ring Theory.zip|
This formalization is concerned with the theory of Gröbner bases in reduction rings.
Gröbner bases constitute one of the key concepts in computer algebra and symbolic computation, as they solve dozens of non-trivial problems in this field in a uniform and elegant way. Originally developed in the setting of polynomial rings over fields, they have been generalized to much broader classes of algebraic structures in the meantime. One of these generalizations are so-called reduction rings: a reduction ring is a commutative ring with unit, not necessarily possessing any polynomial structure or grading, and possibly containing zero divisors, that admit a reasonable definition of Gröbner bases as finite sets that give rise to a certain confluent reduction relation. But not only can Gröbner bases be defined in reduction rings, they can even be computed algorithmically by Buchberger's critical-pair/completion algorithm. Examples of reduction rings (that are all part of this formalization) are all fields, the ring of integers, residue class rings of integers modulo arbitrary n, and multivariate polynomial rings over reduction rings.
The formalization contains all main definitions, theorems and algorithms of the theory, including the definitions of
reduction rings and Gröbner bases in reduction rings, Buchberger's criterion for deciding whether a given set is
a Gröbner basis or not, computable representations of fields, integers, integer residue class rings and polynomial rings,
and a generic, verified implementation of Buchberger's algorithm for effectively computing Gröbner bases in arbitrary
In addition, approximately 50% of the formalization is about elementary mathematical theories, such as sets, numbers, tuples, etc., that only serve as the main building blocks of Gröbner bases- and reduction ring theory, but are themselves completely independent of it.