Abstract
In this paper we present the first-ever computer formalization of the theory of Gröbner bases in reduction rings in Theorema. Not only the formalization, but also the formal verification of all key 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 efficiently exploring mathematical theories: an interactive proving strategy and a “theory analyzer” that already proved extremely useful when creating large structured knowledge bases.
A. Maletzky—This research was funded by the Austrian Science Fund (FWF): grant no. W1214-N15, project DK1.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
As one reviewer pointed out, theory exploration can be understood in several ways. In this paper, we use it as a mere synonym for formalization of mathematical theories.
- 2.
GB is implemented for tuples rather than sets, for practical reasons.
- 3.
- 4.
The first attempt in [3] was erroneous.
- 5.
Once again, this is only true if \(\mathcal {R}\) is a reduction ring and \(\mathcal {T}\) is a domain of commutative power-products.
- 6.
So, there is still some automation of very trivial tasks.
References
Adams, W.W., Loustaunau, P.: An Introduction to Gröbner Bases. Graduate Studies in Mathematics, vol. 3. American Mathematical Society, Providence (1994). doi:10.1090/gsm/003. ISSN: 1065-7339, ISBN: 0-8218-3804-0
Buchberger, B.: A criterion for detecting unnecessary reductions in the construction of Gröbner bases. In: Ng, E.W. (ed.) EUROSAM 1979. LNCS, vol. 72, pp. 3–21. Springer, Heidelberg (1979)
Buchberger, B.: A critical-pair/completion algorithm for finitely generated ideals in rings. In: Börger, E., Hasenjaeger, G., Rödding, D. (eds.) Logic and Machines: Decision Problems and Complexity. LNCS, vol. 171, pp. 137–161. Springer, Heidelberg (1984)
Buchberger, B.: Gröbner Rings in Theorema: A Case Study in Functors and Categories. Technical report 2003–49, Johannes Kepler University Linz, Spezialforschungsbereich F013, November 2003
Buchberger, B., Jebelean, T., Kutsia, T., Maletzky, A., Windsteiger, W.: Theorema 2.0 computer-assisted natural-style mathematics. J. Formalized Reasoning 9(1), 149–185 (2016)
Jorge, J.S., Guilas, V.M., Freire, J.L.: Certifying properties of an efficient functional program for computing Gröbner bases. J. Symbolic Comput. 44(5), 571–582 (2009)
Maletzky, A.: Exploring reduction ring theory in theorema. Technical report 2016–06, Doctoral Program “Computational Mathematics”, Johannes Kepler University Linz, Austria, July 2015
Maletzky, A.: Verifying Buchberger’s algorithm in reduction rings. In: Jebelean, T., Wang, D. (eds.) Proceedings of PAS 2015 (Program Verification, Automated Debugging and Symbolic Computation, Beijing, China, 21–23 October 2015. arXiv:1604.08736
Medina-Bulo, I., Palomo-Lozano, F., Ruiz-Reina, J.L.: A verified common lisp implementation of Buchberger’s algorithm in ACL2. J. Symbolic Comput. 45(1), 96–123 (2010)
Piroi, F., Kutsia, T.: The Theorema environment for interactive proof development. In: Sutcliffe, G., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning. LNCS, vol. 3835, pp. 261–275. Springer, Heidelberg (2005)
Robbiano, L.: Term orderings on the polynomial ring. In: Caviness, B.F. (ed.) EUROCAL 1985. LNCS, vol. 204, pp. 513–517. Springer, Heidelberg (1985)
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.: A generalization of reduction rings. J. Symbolic Comput. 4(3), 351–364 (1988)
Stifter, S.: The reduction ring property is hereditary. J. algebra 140(89–18), 399–414 (1991)
Thery, L.: A machine-checked implementation of Buchberger’s algorithm. J. Autom. Reasoning 26, 107–137 (2001)
Wiesinger-Widi, M.: Gröbner Bases and Generalized Sylvester Matrices. Ph.D. Thesis, Johannes Kepler University Linz (2015). http://epub.jku.at/obvulihs/content/titleinfo/776913
Windsteiger, W.: Building up hierarchical mathematical domains using functors in theorema. In: Armando, A., Jebelean, T. (eds.) Proceedings of Calculemus 1999, Trento, Italy. ENTCS, vol. 23, pp. 401–419. Elsevier, Amsterdam (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)
Winkler, F., Buchberger, B.: A criterion for eliminating unnecessary reductions in the Knuth-Bendix algorithm. In: Colloqium on Algebra, Combinatorics and Logic in Computer Science, pp. 849–869 (1983)
Acknowledgments
I thank the anonymous referees for their valuable remarks and suggestions.
This research was funded by the Austrian Science Fund (FWF): grant no. W1214-N15, project DK1.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Maletzky, A. (2016). Mathematical Theory Exploration in Theorema: Reduction Rings. In: Kohlhase, M., Johansson, M., Miller, B., de Moura, L., Tompa, F. (eds) Intelligent Computer Mathematics. CICM 2016. Lecture Notes in Computer Science(), vol 9791. Springer, Cham. https://doi.org/10.1007/978-3-319-42547-4_1
Download citation
DOI: https://doi.org/10.1007/978-3-319-42547-4_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-42546-7
Online ISBN: 978-3-319-42547-4
eBook Packages: Computer ScienceComputer Science (R0)