Formalizations in Theorema 2.0

Reduction Ring Theory

Abstract

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 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.

Literature

Literature on the Formalization

1. A. Maletzky. Computer-Assisted Exploration of Gröbner Bases Theory in Theorema. PhD thesis, RISC, JKU Linz, May 2016. [pdf]
2. A. Maletzky. Automated Reasoning in Reduction Rings using the Theorema System. In V. P. Gerdt, W. Koepf, W. M. Seiler and E. V. Vorozhtsov, editors, Computer Algebra in Scientific Computing (Proceedings of CASC 2015, Aachen, Germany, September 14-18). LNCS 9301, pages 305-319, Springer, 2015. doi:10.1007/978-3-319-24021-3_23
3. A. Maletzky. Verifying Buchberger's Algorithm in Reduction Rings. In T. Jebelean and D. Wang, editors, Program Verification, Automated Debugging, and Symbolic Computation (Proceedings of PAS 2015, Beijing, China, October 21-23). Pages 16-23, 2015. arXiv:1604.08736 [cs.SC]

Literature on the Underlying Theory

1. B. Buchberger. A Critical-Pair/Completion Algorithm for Finitely Generated Ideals in Rings. In E. Boerger, G. Hasenjaeger, D. Roedding, editors, Logic and Machines: Decision Problems and Complexity (Proceedings of the Symposium "Rekursive Kombinatorik", Münster, Germany, May 23-28). LNCS 171, pages 137-161, Springer, 1984. doi:10.1007/3-540-13331-3_39
2. B. Buchberger. Introduction to Gröbner Bases. In B. Buchberger and F. Winkler, editors, Gröbner Bases and Applications. London Mathematical Society Lecture Notes Series 251, pages 3-31, Cambridge University Press, 1998. [pdf]
3. S. Stifter. A Generalization of Reduction Rings. Journal of Symbolic Computation 4(3):351-364, December 1987. doi:10.1016/S0747-7171(87)80012-3
4. S. Stifter. The Reduction Ring Property is Hereditary. Journal of Algebra 140(2):399-414, July 1991. doi:10.1016/0021-8693(91)90166-6