Refining Algebraic Hierarchy in Mathematical Repository of Mizar

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


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.


  1. 1.
    The ACL2 Sedan Theorem Prover
  2. 2.
    Backer, J., Rudnicki, P., Schwarzweller, C.: Ring ideals. Form. Math. 9(3), 565–582 (2001)Google Scholar
  3. 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).
  4. 4.
    Bancerek, G.: On the structure of Mizar types. Electron. Notes Theor. Comput. Sci. 85(7), Elsevier (2003). Scholar
  5. 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). Scholar
  6. 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). Scholar
  7. 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).
  8. 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).
  9. 9.
    Coghetto, R.: Groups – additive notation. Form. Math. 23(2), 127–160 (2015). Scholar
  10. 10.
    The Coq Proof Assistant
  11. 11.
    Futa, Y., Okazaki, H., Shidama, Y.: Torsion part of \({\mathbb{Z}}\)-module. Formal. Math. 23(4), 297–307 (2015).
  12. 12.
    Geuvers, H., Pollack, R., Wiedijk, F., Zwanenburg, J.: A constructive algebraic hierarchy in Coq. J. Symb. Comput. 34(4), 271–286 (2002). Scholar
  13. 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).
  14. 14.
    Grabowski, A.: Efficient rough set theory merging. Fund. Inf. 135(4), 371–385 (2014). Scholar
  15. 15.
    Grabowski, A.: Mechanizing complemented lattices within Mizar type system. J. Autom. Reason. 55(3), 211–221 (2015). Scholar
  16. 16.
    Grabowski, A.: Stone lattices. Form. Math. 23(4), 387–396 (2015). Scholar
  17. 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). Scholar
  18. 18.
    Grabowski, A., Korniłowicz, A., Naumowicz, A.: Mizar in a nutshell. J. Form. Reas. 3(2), 153–245 (2010).
  19. 19.
    Grabowski, A., Korniłowicz, A., Naumowicz, A.: Four decades of Mizar. J. Autom. Reason. 55(3), 191–198 (2015). Scholar
  20. 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).
  21. 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). Scholar
  22. 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. 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). Scholar
  24. 24.
    The Isabelle Proof Assistant
  25. 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. 26.
    Jenks, R.D., Sutor, R.: AXIOM – The Scientific Computation System. Springer, Berlin (1992).
  27. 27.
    Korniłowicz, A.: Definitional expansions in Mizar. J. Autom. Reason. 55(3), 257–268 (2015). Scholar
  28. 28.
    Korniłowicz, A.: Quotient rings. Form. Math. 13(4), 573–576 (2005)Google Scholar
  29. 29.
    Korniłowicz, A., Rudnicki, P.: The Fundamental Theorem of Arithmetic. Form. Math. 12(2), 179–186 (2004)Google Scholar
  30. 30.
    Korniłowicz, A., Schwarzweller, C.: The first isomorphism theorem and other properties of rings. Form. Math. 22(4), 291–302 (2014). Scholar
  31. 31.
    Milewski, R.: The ring of polynomials. Form. Math. 9(2), 339–346 (2001)Google Scholar
  32. 32.
    The Mizar Home Page
  33. 33.
    The Mizar Library Committee, Basic algebraic structures. MML Id: ALGSTR_0 (2007).
  34. 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). Scholar
  35. 35.
    Pa̧k, K.: Methods of lemma extraction in natural deduction proofs. J. Autom. Reason. 50(2), 217–228 (2013).
  36. 36.
    Rabe, F. Kohlhase, M.: A scalable module system. Inf. Comput. 230, 1–54 (2013). Scholar
  37. 37.
    Rudnicki, P., Trybulec, A., Schwarzweller, C.: Commutative algebra in the Mizar system. J. Symb. Comput. 32(1/2), 143–169 (2001). Scholar
  38. 38.
    Schwarzweller, C.: The ring of integers, Euclidean rings and modulo integers. Form. Math. 8(1), 29–34 (1999)Google Scholar
  39. 39.
    Schwarzweller, C.: Designing mathematical libraries based on requirements for theorems. Ann. Math. Artif. Intell. 38(1–3), 193–209 (2003).
  40. 40.
    Schwarzweller, C., Korniłowicz, A., Rowinska-Schwarzweller, A.: Some algebraic properties of polynomial ring. Form. Math. 24(3), 227–237 (2016). Scholar
  41. 41.
    Weintraub, S.H.: Galois Theory, 2nd edn. Springer, Berlin (2009)CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.Institute of InformaticsUniversity of BiałystokBiałystokPoland
  2. 2.Department of Computer ScienceUniversity of GdańskGdańskPoland

Personalised recommendations