-
Verifying Buchberger's Algorithm in Reduction Rings
Authors:
Alexander Maletzky
Abstract:
In this paper we present the formal, computer-supported verification of a functional implementation of Buchberger's critical-pair/completion algorithm for computing Gröbner bases in reduction rings. We describe how the algorithm can be implemented and verified within one single software system, which in our case is the Theorema system.
In contrast to existing formal correctness proofs of Buchber…
▽ More
In this paper we present the formal, computer-supported verification of a functional implementation of Buchberger's critical-pair/completion algorithm for computing Gröbner bases in reduction rings. We describe how the algorithm can be implemented and verified within one single software system, which in our case is the Theorema system.
In contrast to existing formal correctness proofs of Buchberger's algorithm in other systems, e. g. Coq and ACL2, our work is not confined to the classical setting of polynomial rings over fields, but considers the much more general setting of reduction rings; this, naturally, makes the algorithm more complicated and the verification more difficult.
The correctness proof is essentially based on some non-trivial results from the theory of reduction rings, which we formalized and formally proved as well. This formalization already consists of more than 800 interactively proved lemmas and theorems, making the elaboration an extensive example of higher-order theory exploration in Theorema.
△ Less
Submitted 29 April, 2016;
originally announced April 2016.
-
Mathematical Theory Exploration in Theorema: Reduction Rings
Authors:
Alexander Maletzky
Abstract:
In this paper we present the first-ever computer formalization of the theory of Gröbner bases in reduction rings, which is an important theory in computational commutative algebra, in Theorema. Not only the formalization, but also the formal verification of all results has already been fully completed by now; this, in particular, includes the generic implementation and correctness proof of Buchber…
▽ More
In this paper we present the first-ever computer formalization of the theory of Gröbner bases in reduction rings, which is an important theory in computational commutative algebra, in Theorema. Not only the formalization, but also the formal verification of all results has already been fully completed by now; this, in particular, includes the generic implementation and correctness proof of Buchberger's algorithm in reduction rings. Thanks to the seamless integration of proving and computing in Theorema, this implementation can now be used to compute Gröbner bases in various different domains directly within the system. Moreover, a substantial part of our formalization is made up solely by "elementary theories" such as sets, numbers and tuples that are themselves independent of reduction rings and may therefore be used as the foundations of future theory explorations in Theorema.
In addition, we also report on two general-purpose Theorema tools we developed for an efficient and convenient exploration of mathematical theories: an interactive proving strategy and a "theory analyzer" that already proved extremely useful when creating large structured knowledge bases.
△ Less
Submitted 13 February, 2016;
originally announced February 2016.
-
Two-Point Boundary Problems with One Mild Singularity and an Application to Graded Kirchhoff Plates
Authors:
M. Rosenkranz,
J. Liu,
A. Maletzky,
B. Buchberger
Abstract:
We develop a new theory for treating boundary problems for linear ordinary differential equations whose fundamental system may have a singularity at one of the two endpoints of the given interval. Our treatment follows an algebraic approach, with (partial) implementation in the Theorema software system (which is based on Mathematica). We study an application to graded Kirchhoff plates for illustra…
▽ More
We develop a new theory for treating boundary problems for linear ordinary differential equations whose fundamental system may have a singularity at one of the two endpoints of the given interval. Our treatment follows an algebraic approach, with (partial) implementation in the Theorema software system (which is based on Mathematica). We study an application to graded Kirchhoff plates for illustrating a typical case of such boundary problems.
△ Less
Submitted 8 May, 2015;
originally announced May 2015.
