Skip to main content
SpringerLink
Log in

Refining Algebraic Hierarchy in Mathematical Repository of Mizar

  • Chapter
  • First Online:
AI Aspects in Reasoning, Languages, and Computation

Part of the book series: Studies in Computational Intelligence ((SCI,volume 889))

Abstract

Mathematics, especially algebra, uses plenty of structures: groups, rings, integral domains, fields, vector spaces to name a few of the most basic ones. Classes of structures are closely connected—usually by inclusion—naturally leading to hierarchies that has been reproduced in different forms in different mathematical repositories. We give a brief overview of some existing algebraic hierarchies and report on the latest developments in the Mizar computerized proof assistant system. In particular we present a detailed algebraic hierarchy that has been defined in Mizar and discuss extensions of the hierarchy towards more involved domains, using internal mechanisms available in the system.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

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 119.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 159.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 159.99
Price excludes VAT (USA)
  • Durable hardcover 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

Institutional subscriptions

References

  1. The ACL2 Sedan Theorem Prover http://acl2s.ccs.neu.edu/acl2s/doc/

  2. Backer, J., Rudnicki, P., Schwarzweller, C.: Ring ideals. Form. Math. 9(3), 565–582 (2001)

    Google Scholar 

  3. Ballarin, C.: Interpretation of locales in Isabelle: theories and proof contexts. In: Borwein, J.M., Farmer W.M. (eds.) 5th International Conference on Mathematical Knowledge Management, MKM 2006. Lecture Notes in Computer Science, vol. 4108, pp. 31–43. Springer (2006). https://dx.doi.org/10.1007/11812289_4

  4. Bancerek, G.: On the structure of Mizar types. Electron. Notes Theor. Comput. Sci. 85(7), Elsevier (2003). https://dx.doi.org/10.1016/S1571-0661(04)80758-8

    Article  Google Scholar 

  5. Bancerek, G., Byliński, C., Grabowski, A., Korniłowicz, A., Matuszewski, R., Naumowicz, A., Pa̧k, K., Urban, J.: Mizar: State-of-the-art and beyond. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge V. (eds.) Intelligent Computer Mathematics – International Conference, CICM 2015, Washington, DC, USA, July 13–17, 2015. Proceedings, Lecture Notes in Computer Science, vol. 9150, pp. 261–279. Springer (2015). https://dx.doi.org/10.1007/978-3-319-20615-8_17

    Google Scholar 

  6. Bancerek, G., Byliński, C., Grabowski, A., Korniłowicz, A., Matuszewski, R., Naumowicz, A., Pa̧k, K.: The role of the Mizar Mathematical Library for interactive proof development in Mizar. J. Autom. Reason. 61(1), 9–32 (2018). https://dx.doi.org/10.1007/s10817-017-9440-6

    Article  MathSciNet  Google Scholar 

  7. Carette, J., Farmer, W.M., Kohlhase, M.: Realms: a structure for consolidating knowledge about mathematical theories. In: Watt S. et al. (eds.) International Conference on Intelligent Computer Mathematics – Proceedings. Lecture Notes in Computer Science, vol. 8543, pp. 252–266. Springer (2014). https://dx.doi.org/10.1007/978-3-319-08434-3_19

  8. Carette, J., O’Connor, R.: Theory presentation combinators. In: Jeuring, J. et al. (eds.) International Conference on Intelligent Computer Mathematics – Proceedings. Lecture Notes in Computer Science, vol. 7362, pp. 202–215. Springer (2013). https://dx.doi.org/10.1007/978-3-642-31374-5_14

  9. Coghetto, R.: Groups – additive notation. Form. Math. 23(2), 127–160 (2015). https://dx.doi.org/10.1515/forma-2015-0013

    Article  Google Scholar 

  10. The Coq Proof Assistant http://coq.inria.fr

  11. Futa, Y., Okazaki, H., Shidama, Y.: Torsion part of \({\mathbb{Z}}\)-module. Formal. Math. 23(4), 297–307 (2015). https://dx.doi.org/10.1515/forma-2015-0024

  12. Geuvers, H., Pollack, R., Wiedijk, F., Zwanenburg, J.: A constructive algebraic hierarchy in Coq. J. Symb. Comput. 34(4), 271–286 (2002). https://dx.doi.org/10.1006/jsco.2002.0552

    Article  MathSciNet  Google Scholar 

  13. Gonthier, G. et al.: A machine-checked proof of the Odd Order Theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie D. (eds.) Proceedings of the 4th International Conference on Interactive Theorem Proving. Lecture Notes in Computer Science, vol. 7998, pp. 163–179. Springer (2013). https://dx.doi.org/10.1007/978-3-642-39634-2_14

  14. Grabowski, A.: Efficient rough set theory merging. Fund. Inf. 135(4), 371–385 (2014). https://dx.doi.org/10.3233/FI-2014-1129

    Article  MathSciNet  Google Scholar 

  15. Grabowski, A.: Mechanizing complemented lattices within Mizar type system. J. Autom. Reason. 55(3), 211–221 (2015). https://dx.doi.org/10.1007/s10817-015-9333-5

    Article  MathSciNet  Google Scholar 

  16. Grabowski, A.: Stone lattices. Form. Math. 23(4), 387–396 (2015). https://dx.doi.org/10.2478/forma-2015-0031

    Article  Google Scholar 

  17. Grabowski, A.: Expressing the notion of a mathematical structure in the formal language of Mizar. In: Gruca, A., Czachórski, T., Harezlak, K., Kozielski, S., Piotrowska, A. (eds.) Man–Machine Interactions 5, ICMMI 2017. Advances in Intelligent Systems and Computing, vol. 659, pp. 261–270. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-67792-7_26

    Google Scholar 

  18. Grabowski, A., Korniłowicz, A., Naumowicz, A.: Mizar in a nutshell. J. Form. Reas. 3(2), 153–245 (2010). https://dx.doi.org/10.6092/issn.1972-5787/1980

  19. Grabowski, A., Korniłowicz, A., Naumowicz, A.: Four decades of Mizar. J. Autom. Reason. 55(3), 191–198 (2015). https://dx.doi.org/10.1007/s10817-015-9345-1

    Article  MathSciNet  Google Scholar 

  20. Grabowski, A., Korniłowicz, A., Schwarzweller, C.: Equality in computer proof-assistants. In: Ganzha, M., Maciaszek, L., Paprzycki., M. (eds.) Proceedings of 2015 Federated Conference on Computer Science and Information Systems, FedCSIS 2015, pp. 45–54. IEEE (2015). https://dx.doi.org/10.15439/2015F229

  21. Grabowski, A., Schwarzweller, C.: Revisions as an essential tool to maintain mathematical repositories. In: Kauers, M., Kerber, M., Miner, R., Windsteiger W. (eds.) Towards Mechanized Mathematical Assistants, 6th International Conference, MKM 2007, Calculemus 2007. Lecture Notes in Computer Science, vol. 4573, pp. 235–249. Springer, Berlin (2007). https://dx.doi.org/10.1007/978-3-540-73086-6_20

    Chapter  Google Scholar 

  22. Grabowski, A., Schwarzweller, C.: Towards standard environments for formalizing mathematics. In: Gomolińska, A., Grabowski, A., Hryniewicka, M., Kacprzak, M., Schmeidel, E. (eds.) Proceedings of the 6th Podlasie Conference on Mathematics, Białystok, Poland (2014)

    Google Scholar 

  23. Heras, J., Martín-Mateos, F.J., Pascual, V.: Modelling algebraic structures and morphisms in ACL2. Appl. Algebr. Eng., Commun. Comput. 26(3), 277–303 (2015). https://dx.doi.org/10.1007/s00200-015-0252-9

    Article  MathSciNet  Google Scholar 

  24. The Isabelle Proof Assistant http://isabelle.in.tum.de

  25. Jackson, P.B.: Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra, PhD thesis, Cornell University (1995)

    Google Scholar 

  26. Jenks, R.D., Sutor, R.: AXIOM – The Scientific Computation System. Springer, Berlin (1992). https://dx.doi.org/10.1007/978-1-4612-2940-7

  27. Korniłowicz, A.: Definitional expansions in Mizar. J. Autom. Reason. 55(3), 257–268 (2015). https://dx.doi.org/10.1007/s10817-015-9331-7

    Article  MathSciNet  Google Scholar 

  28. Korniłowicz, A.: Quotient rings. Form. Math. 13(4), 573–576 (2005)

    Google Scholar 

  29. Korniłowicz, A., Rudnicki, P.: The Fundamental Theorem of Arithmetic. Form. Math. 12(2), 179–186 (2004)

    Google Scholar 

  30. Korniłowicz, A., Schwarzweller, C.: The first isomorphism theorem and other properties of rings. Form. Math. 22(4), 291–302 (2014). https://dx.doi.org/10.2478/forma-2014-0029

    Article  Google Scholar 

  31. Milewski, R.: The ring of polynomials. Form. Math. 9(2), 339–346 (2001)

    Google Scholar 

  32. The Mizar Home Page http://mizar.org

  33. The Mizar Library Committee, Basic algebraic structures. MML Id: ALGSTR_0 (2007). https://mizar.org/version/current/html/algstr_0.html

  34. Naumowicz, A.: Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver. J. Autom. Reason. 55(3), 285–294 (2015). https://dx.doi.org/10.1007/s10817-015-9332-6

    Article  MathSciNet  Google Scholar 

  35. Pa̧k, K.: Methods of lemma extraction in natural deduction proofs. J. Autom. Reason. 50(2), 217–228 (2013). https://dx.doi.org/10.1007/s10817-012-9267-0

  36. Rabe, F. Kohlhase, M.: A scalable module system. Inf. Comput. 230, 1–54 (2013). https://dx.doi.org/10.1016/j.ic.2013.06.001

    Article  MathSciNet  Google Scholar 

  37. Rudnicki, P., Trybulec, A., Schwarzweller, C.: Commutative algebra in the Mizar system. J. Symb. Comput. 32(1/2), 143–169 (2001). https://dx.doi.org/10.1006/jsco.2001.0456

    Article  MathSciNet  Google Scholar 

  38. Schwarzweller, C.: The ring of integers, Euclidean rings and modulo integers. Form. Math. 8(1), 29–34 (1999)

    Google Scholar 

  39. Schwarzweller, C.: Designing mathematical libraries based on requirements for theorems. Ann. Math. Artif. Intell. 38(1–3), 193–209 (2003). https://dx.doi.org/10.1023/A:1022924032739

  40. Schwarzweller, C., Korniłowicz, A., Rowinska-Schwarzweller, A.: Some algebraic properties of polynomial ring. Form. Math. 24(3), 227–237 (2016). https://dx.doi.org/10.1515/forma-2016-0019

    Article  Google Scholar 

  41. Weintraub, S.H.: Galois Theory, 2nd edn. Springer, Berlin (2009)

    Book  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Informatics, University of Białystok, ul. Ciołkowskiego 1 M, 15-245, Białystok, Poland

    Adam Grabowski & Artur Korniłowicz

  2. Department of Computer Science, University of Gdańsk, ul. Wita Stwosza 57, 80-952, Gdańsk, Poland

    Christoph Schwarzweller

Authors
  1. Adam Grabowski
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Artur Korniłowicz
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Christoph Schwarzweller
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Adam Grabowski .

Editor information

Editors and Affiliations

  1. Institute of Informatics, University of Bialystok, Bialystok, Poland

    Adam Grabowski

  2. Department of Mathematics, Stockholm University, Stockholm, Sweden

    Roussanka Loukanova

  3. Institute of Informatics, University of Gdansk, Gdańsk, Poland

    Christoph Schwarzweller

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Grabowski, A., Korniłowicz, A., Schwarzweller, C. (2020). Refining Algebraic Hierarchy in Mathematical Repository of Mizar. In: Grabowski, A., Loukanova, R., Schwarzweller, C. (eds) AI Aspects in Reasoning, Languages, and Computation. Studies in Computational Intelligence, vol 889. Springer, Cham. https://doi.org/10.1007/978-3-030-41425-2_2

Download citation

Publish with us

Policies and ethics

Search

Navigation