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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Buchberger, B.: A critical-pair/completion algorithm for finitely generated ideals in rings. In: Börger, E., Rödding, D., Hasenjaeger, G. (eds.) Rekursive Kombinatorik 1983. LNCS, vol. 171, pp. 137–161. Springer, Heidelberg (1984)
Buchberger, B.: Gröbner Rings in Theorema: A Case Study in Functors and Categories. Tech. Rep. 2003–49, RISC Report Series, Johannes Kepler University Linz, Austria (2003)
Buchberger, B.: Towards the automated synthesis of a Gröbner bases Algorithm. RACSAM (Revista de la Real Academia de Ciencias), Serie A: Mathematicas 98(1), 65–75 (2004)
Buchberger, B., Craciun, A., Jebelean, T., Kovacs, L., Kutsia, T., Nakagawa, K., Piroi, F., Popov, N., Robu, J., Rosenkranz, M., Windsteiger, W.: Theorema: Towards computer-aided mathematical theory exploration. J. Applied Logic 4(4), 470–504 (2006)
Craciun, A.: Lazy Thinking Algorithm Synthesis in Gröbner Bases Theory. PhD thesis, RISC, Johannes Kepler University Linz, Austria (2008)
Jorge, J.S., Guilas, V.M., Freire, J.L.: Certifying properties of an efficient functional program for computing Gröbner bases. J. Symbolic Computation 44(5), 571–582 (2009)
Medina-Bulo, I., Palomo-Lozano, F., Ruiz-Reina, J.-L.: A verified Common Lisp implementation of Buchberger’s algorithm in ACL2. J. Symbolic Computation 45(1), 96–123 (2010)
Robu, J., Ida, T., Ţepeneu, D., Takahashi, H., Buchberger, B.: Computational origami construction of a regular heptagon with automated proof of its correctness. In: Hong, H., Wang, D. (eds.) ADG 2004. LNCS (LNAI), vol. 3763, pp. 19–33. Springer, Heidelberg (2006)
Robu, J.: Automated proof of geometry theorems involving order relation in the frame of the theorema project. In: Pop, H.F. (ed.) KEPT 2007 (Knowledge Engineering, Principles and Techniques). Special issue of Studia Universitatis ”Babes-Bolyai”, Series Informatica, pp. 307–315 (2007)
Rosenkranz, M.: A new symbolic method for solving linear two-point boundary value problems on the level of operators. J. Symbolic Computation 39(2), 171–199 (2005)
Schwarzweller, C.: Gröbner bases – theory refinement in the mizar system. In: Kohlhase, M. (ed.) MKM 2005. LNCS (LNAI), vol. 3863, pp. 299–314. Springer, Heidelberg (2006)
Stifter, S.: Computation of Gröbner Bases over the Integers and in General Reduction Rings. Diploma thesis, Institut für Mathematik, Johannes Kepler University Linz, Austria (1985)
Stifter, S.: The reduction ring property is hereditary. J. Algebra 140(89–18), 399–414 (1991)
Tec, L.: A Symbolic Framework for General Polynomial Domains in Theorema: Applications to Boundary Problems. PhD thesis, RISC, Johannes Kepler University Linz, Austria (2011)
Thery, L.: A machine-checked implementation of Buchberger’s Aalgorithm. J. Automated Reasoning 26, 107–137 (2001)
Wiesinger-Widi, M.: Gröbner Bases and Generalized Sylvester Matrices. PhD thesis, RISC, Johannes Kepler University Linz, Austria (2015 to appear)
Windsteiger, W.: Building up hierarchical mathematical domains using functors in theorema. In: Armando, A., Jebelean, T. (eds.) Calculemus 1999. ENTCS, vol. 23, pp. 401–419. Elsevier (1999)
Windsteiger, W.: Theorema 2.0: a system for mathematical theory exploration. In: Hong, H., Yap, C. (eds.) ICMS 2014. LNCS, vol. 8592, pp. 49–52. Springer, Heidelberg (2014)
The theorema System. http://www.risc.jku.at/research/theorema/software/
Wolfram Mathematica. http://www.wolfram.com/mathematica/
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Maletzky, A. (2015). Automated Reasoning in Reduction Rings Using the Theorema System. In: Gerdt, V., Koepf, W., Seiler, W., Vorozhtsov, E. (eds) Computer Algebra in Scientific Computing. CASC 2015. Lecture Notes in Computer Science(), vol 9301. Springer, Cham. https://doi.org/10.1007/978-3-319-24021-3_23
Download citation
DOI: https://doi.org/10.1007/978-3-319-24021-3_23
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-24020-6
Online ISBN: 978-3-319-24021-3
eBook Packages: Computer ScienceComputer Science (R0)