Skip to main content
SpringerLink
Log in
Book cover

International Conference on Intelligent Computer Mathematics

CICM 2016: Intelligent Computer Mathematics pp 3–17Cite as

Mathematical Theory Exploration in Theorema: Reduction Rings

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 9791))

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.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   34.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   44.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

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

    GB is implemented for tuples rather than sets, for practical reasons.

  3. 3.

    For information on functors and domains in Theorema, see [4, 17].

  4. 4.

    The first attempt in [3] was erroneous.

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

    So, there is still some automation of very trivial tasks.

References

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

    MATH  Google Scholar 

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

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

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

    Google Scholar 

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

    MathSciNet  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  7. Maletzky, A.: Exploring reduction ring theory in theorema. Technical report 2016–06, Doctoral Program “Computational Mathematics”, Johannes Kepler University Linz, Austria, July 2015

    Google Scholar 

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

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Chapter  Google Scholar 

  11. Robbiano, L.: Term orderings on the polynomial ring. In: Caviness, B.F. (ed.) EUROCAL 1985. LNCS, vol. 204, pp. 513–517. Springer, Heidelberg (1985)

    Google Scholar 

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

    Chapter  Google Scholar 

  13. Stifter, S.: A generalization of reduction rings. J. Symbolic Comput. 4(3), 351–364 (1988)

    Article  MathSciNet  MATH  Google Scholar 

  14. Stifter, S.: The reduction ring property is hereditary. J. algebra 140(89–18), 399–414 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  15. Thery, L.: A machine-checked implementation of Buchberger’s algorithm. J. Autom. Reasoning 26, 107–137 (2001)

    Article  MathSciNet  MATH  Google Scholar 

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

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

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

Download references

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

  1. Doctoral Program “Computational Mathematics” and RISC, Johannes Kepler University, Linz, Austria

    Alexander Maletzky

Authors
  1. Alexander Maletzky
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Alexander Maletzky .

Editor information

Editors and Affiliations

  1. Jacobs University Bremen, Bremen, Germany

    Michael Kohlhase

  2. Chalmers University, Göteborg, Sweden

    Moa Johansson

  3. National Institute of Standards and Technology, Gaithersburg, Maryland, USA

    Bruce Miller

  4. Microsoft Research, Redmond, Washington, USA

    Leonardo de Moura

  5. University of Waterloo, Waterloo, Ontario, Canada

    Frank Tompa

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation