Logo PTI
Polish Information Processing Society
Logo FedCSIS

Annals of Computer Science and Information Systems, Volume 8

Proceedings of the 2016 Federated Conference on Computer Science and Information Systems

On algebraic hierarchies in mathematical repository of Mizar

, ,

DOI: http://dx.doi.org/10.15439/2016F520

Citation: Proceedings of the 2016 Federated Conference on Computer Science and Information Systems, M. Ganzha, L. Maciaszek, M. Paprzycki (eds). ACSIS, Vol. 8, pages 363–371 ()

Full text

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. In this paper 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. Taking fully formal approach into account we meet new difficulties comparing with its informal mathematical framework.

References

  1. The ACL2 Sedan Theorem Prover; available at http://acl2s.ccs.neu.edu/acl2s/doc/
  2. J. Backer, P. Rudnicki, and C. Schwarzweller, Ring Ideals; Formalized Mathematics, vol. 9(3), pp. 565–582, 2001.
  3. C. Ballarin, Interpretation of Locales in Isabelle: Theories and Proof Contexts; in: 5th International Conference on Mathematical Knowledge Management, MKM 2006, Lecture Notes in Computer Science, 4108, pp. 31–43, 2006. http://dx.doi.org/10.1007/11812289_4
  4. G. Bancerek, On the Structure of Mizar Types, Electronic Notes in Theoretical Computer Science, vol. 85 (7), Elsevier, 2003. http://dx.doi.org/10.1016/S1571-0661(04)80758-8
  5. G. Bancerek, C. Byliński, A. Grabowski, A. Korniłowicz, R. Ma-tuszewski, A. Naumowicz, K. Pąk, and J. Urban, Mizar: State-of-the-art and Beyond, in: M. Kerber, J. Carette, C. Kaliszyk, F. Rabe, and V. Sorge (eds.), International Conference on Intelligent Computer Mathematics – Proceedings, Lecture Notes in Computer Science 9150, pp. 261–279, 2015. http://dx.doi.org/10.1007/978-3-319-20615-8_17
  6. J. Carette, W.M. Farmer, and M. Kohlhase, Realms: A Structure for Consolidating Knowledge about Mathematical Theories, in: S. Watt et al. (eds.), International Conference on Intelligent Computer Mathematics – Proceedings, Lecture Notes in Computer Science 8543, pp. 252–266, 2014. http://dx.doi.org/10.1007/978-3-319-08434-3_19
  7. J. Carette and R. O’Connor, Theory Presentation Combinators, in: J. Jeuring et al. (eds.), International Conference on Intelligent Computer Mathematics – Proceedings, Lecture Notes in Computer Science 7362, pp. 202–215, 2013. http://dx.doi.org/10.1007/978-3-642-31374-5_14
  8. R. Coghetto, Groups – Additive Notation; Formalized Mathematics, vol. 23(2), pp. 127–160, 2015. http://dx.doi.org/10.1515/forma-2015-0013
  9. The Coq Proof Assistant; available at http://coq.inria.fr.
  10. Y. Futa, H. Okazaki, and Y. Shidama, Torsion Part of Z-module; Formalized Mathematics, vol. 23(4), pp. 297–307, 2015. http://dx.doi.org/10.1515/forma-2015-0024
  11. H. Geuvers, R. Pollack, F. Wiedijk, and J. Zwanenburg, A Constructive Algebraic Hierarchy in Coq; Journal of Symbolic Computation, vol. 34(4), pp. 271–286, 2002. http://dx.doi.org/10.1006/jsco.2002.0552
  12. G. Gonthier et al., A Machine-Checked Proof of the Odd Order Theorem; in: S. Blazy, C. Paulin-Mohring, D. Pichardie (eds.), Proceedings of the 4th International Conference on Interactive Theorem Proving, Lecture Notes in Computer Science 7998, pp. 163–179, 2013. http://dx.doi.org/10.1007/978-3-642-39634-2_14
  13. A. Grabowski, Efficient Rough Set Theory Merging; Fundamenta Informaticae, 135(4), pp. 371–385, 2014. http://dx.doi.org/10.3233/FI-2014-1129
  14. A. Grabowski, Mechanizing Complemented Lattices Within Mizar Type System; Journal of Automated Reasoning, vol. 55(3), pp. 211–221, 2015. http://dx.doi.org/10.1007/s10817-015-9333-5
  15. A. Grabowski, Stone Lattices; Formalized Mathematics, vol. 23(4), pp. 387–396, 2015. http://dx.doi.org/10.2478/forma-2015-0031
  16. A. Grabowski, A. Korniłowicz, and A. Naumowicz, Mizar in a Nutshell; Journal of Formalized Reasoning, 3(2), pp. 153–245, 2010. http://dx.doi.org/10.6092/issn.1972-5787/1980
  17. A. Grabowski, A. Korniłowicz, and A. Naumowicz, Four decades of Mizar; Journal of Automated Reasoning, vol. 55(3), pp. 191–198, 2015. http://dx.doi.org/10.1007/s10817-015-9345-1
  18. A. Grabowski, A. Korniłowicz, and C. Schwarzweller, Equality in computer proof-assistants; in Proceedings of 2015 Federated Conference on Computer Science and Information Systems, FedCSIS 2015, M. Ganzha, L. Maciaszek, M. Paprzycki (eds.), IEEE, pp. 45–54, 2015. http://dx.doi.org/10.15439/2015F229
  19. A. Grabowski and C. Schwarzweller, Revisions as an essential tool to maintain mathematical repositories; in: 14th Symposium on Towards Mechanized Mathematical Assistants, Calculemus’07/MKM’07, Lecture Notes in Computer Science, pp. 235–249, 2007 http://dx.doi.org/10.1007/978-3-540-73086-6_20
  20. A. Grabowski and C. Schwarzweller, Towards Standard Environments for Formalizing Mathematics; in: Proceedings of the 6th Podlasie Conference on Mathematics, A. Gomolinska, A. Grabowski, M. Hryniewicka, M. Kacprzak, E.Schmeidel (eds.), Białystok, Poland, 2014.
  21. J. Heras, F.J. Martín-Mateos, and V. Pascual, Modelling Algebraic Structures and Morphisms in ACL2; Applicable Algebra in Engineering, Communication and Computing, vol. 26(3), pp. 277–303, 2015. http://dx.doi.org/10.1007/s00200-015-0252-9
  22. The Isabelle Proof Assistant; available at isabelle.in.tum.de.
  23. P.B. Jackson, Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra; PhD thesis, Cornell University, 1995.
  24. R.D. Jenks and R. Sutor, AXIOM – The Scientific Computation System; Springer Verlag, 1992. http://dx.doi.org/10.1007/978-1-4612-2940-7
  25. A. Korniłowicz, Definitional Expansions in Mizar; Journal of Automated Reasoning, vol. 55(3), pp. 257–268, 2015. http://dx.doi.org/10.1007/s10817-015-9331-7
  26. A. Korniłowicz, Quotient Rings; Formalized Mathematics, vol. 13(4), pp. 573–576, 2005.
  27. A. Korniłowicz and P. Rudnicki, The Fundamental Theorem of Arithmetic; Formalized Mathematics, vol. 12(2), pp. 179–186, 2004.
  28. A. Korniłowicz and C. Schwarzweller, The First Isomorphism Theorem and Other Properties of Rings; Formalized Mathematics, vol. 22(4), pp. 291–302, 2014. http://dx.doi.org/10.2478/forma-2014-0029
  29. R. Milewski, The Ring of Polynomials; Formalized Mathematics, vol. 9(2), pp. 339–346, 2001.
  30. The Mizar Library Committee, Basic Algebraic Structures; 2007. MML Id: ALGSTR_0, available at http://mizar.org/version/current/html/algstr_0.html
  31. The Mizar Home Page; available at http://mizar.org.
  32. A. Naumowicz, Automating Boolean Set Operations in Mizar Proof Checking with the Aid of an External SAT Solver; Journal of Automated Reasoning, vol. 55(3), pp. 285–294, 2015. http://dx.doi.org/10.1007/s10817-015-9332-6
  33. Pak ̨ K.: Methods of Lemma Extraction in Natural Deduction Proofs, Journal of Automated Reasoning, vol. 50(2), pp. 217–228, 2013. http://dx.doi.org/10.1007/s10817-012-9267-0
  34. F. Rabe and M. Kohlhase, A Scalable Module System, Information & Computation, 230, pp. 1–54, 2013. http://dx.doi.org/10.1016/j.ic.2013.06.001
  35. P. Rudnicki, A. Trybulec, and C. Schwarzweller, Commutative Algebra in the Mizar System; Journal of Symbolic Computation, vol. 32(1/2), pp. 143–169, 2001. http://dx.doi.org/10.1006/jsco.2001.0456
  36. C. Schwarzweller, The Ring of Integers, Euclidean Rings and Modulo Integers; Formalized Mathematics, vol. 8(1), pp. 29–34, 1999.
  37. C. Schwarzweller, Designing Mathematical Libraries based on Requirements for Theorems; Annals of Mathematics and Artificial Intelligence, vol. 38(1–3), pp. 193–209, 2003. http://dx.doi.org/10.1023/A:1022924032739
  38. C. Schwarzweller, A. Korniłowicz, and A. Rowinska-Schwarzweller, Some Algebraic Properties of Polynomial Ring; Formalized Mathematics, vol. 24(3), 2016. http://dx.doi.org/10.1515/forma-2016-0019
  39. S.H. Weintraub, Galois Theory; 2nd edition, Springer Verlag, 2009.