Automated Reasoning in Reduction Rings Using the Theorema System

Abstract. In this paper we present the computer-supported theory exploration, including both formalization and verification, of a theory in commutative algebra, namely the theory of reduction rings. Reduction rings, introduced by Bruno Buchberger in 1984, are commutative rings with unit which extend classical Gröbner bases theory from polynomial rings over fields to a far more general setting. We review some of the most important notions and concepts in the theory and motivate why reduction rings are a natural candidate for being explored with the assistance of a software system, which, in our case, is the Theorema system. We also sketch the special prover designed and implemented for the purpose of semi-automated, interactive verification of the theory, and outline the structure of the formalization.

• Type: Journal
• Year: 2015
• Where: CASC
• Authors: Alexander Maletzky
• Keywords: CASC 2015, Mathematics