Keywords  Gröbner bases, Buchberger's algorithm, reduction rings 
Put online  April 22, 2016 
Size  43.1 MB (zipped), 760.5 MB (unzipped) 
SubTheories (15) 

Depends on   
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 nontrivial 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 socalled 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 criticalpair/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
reduction rings.
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.