Logo PTI
Polish Information Processing Society
Logo FedCSIS

Annals of Computer Science and Information Systems, Volume 11

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

Progress in the Independent Certification of Mizar Mathematical Library in Isabelle

,

DOI: http://dx.doi.org/10.15439/2017F289

Citation: Proceedings of the 2017 Federated Conference on Computer Science and Information Systems, M. Ganzha, L. Maciaszek, M. Paprzycki (eds). ACSIS, Vol. 11, pages 227–236 ()

Full text

Abstract. The Mizar Mathematical Library is one of the largest collections of machine understandable formal proofs encompassing many areas of today mathematics including results from algebra, analysis, topology, and lattice theory. The Mizar system has so far been the only tool able to completely process, certify, and make use of these developments. In this paper, we present the progress in the development of an independent certification mechanism of Mizar proofs based on the Isabelle logical framework. The approach allows rechecking the Mizar formal proofs based on a more succinct and more precisely specified formal infrastructure. Additionally, it necessitates a full formal specification of the mechanisms that ensure the correctness of the defined objects, in particular, the proofs that such mechanisms are correct. The development already covers an important part of the Mizar library foundations. We improve the mechanism for defining Mizar structures and show that it permits simpler validation of proof developments involving such objects. To demonstrate this, we perform a complete translation of the Mizar net of basic algebraic structures including their attributes and certify all the corresponding proofs in Isabelle.

References

  1. X. Leroy, “Formal verification of a realistic compiler,” Commun. ACM, vol. 52, no. 7, pp. 107–115, 2009. http://dx.doi.org/10.1145/1538788.1538814
  2. G. Klein, J. Andronick, K. Elphinstone, T. C. Murray, T. Sewell, R. Kolanski, and G. Heiser, “Comprehensive formal verification of an OS microkernel,” ACM Trans. Comput. Syst., vol. 32, no. 1, p. 2, 2014. http://dx.doi.org/10.1145/2560537
  3. J. Harrison, “Floating-Point Verification,” J. UCS, vol. 13, no. 5, pp. 629–638, 2007. http://dx.doi.org/10.3217/jucs-013-05-0629
  4. T. C. Hales, M. Adams, G. Bauer, D. T. Dang, J. Harrison, T. L. Hoang, C. Kaliszyk, V. Magron, S. McLaughlin, T. T. Nguyen, T. Q. Nguyen, T. Nipkow, S. Obua, J. Pleso, J. Rute, A. Solovyev, A. H. T. Ta, T. N. Tran, D. T. Trieu, J. Urban, K. K. Vu, and R. Zumkeller, “A formal proof of the Kepler conjecture,” Forum of Mathematics, Pi, vol. 5, 2017. http://dx.doi.org/10.1017/fmp.2017.1
  5. G. Bancerek, C. Bylinski, A. Grabowski, A. Korniłowicz, R. Matuszewski, A. Naumowicz, K. Pąk, and J. Urban, “Mizar: State-of- the-art and Beyond,” in Intelligent Computer Mathematics - International Conference, CICM 2015, ser. LNCS, M. Kerber, J. Carette, C. Kaliszyk, F. Rabe, and V. Sorge, Eds., vol. 9150. Springer, 2015. http://dx.doi.org/10.1007/978-3-319-20615-8_17 pp. 261–279.
  6. J. Alama, M. Kohlhase, L. Mamane, A. Naumowicz, P. Rudnicki, and J. Urban, “Licensing the Mizar Mathematical Library,” in Proc. 10th International Conference on Intelligent Computer Mathematics (CICM 2011), ser. LNCS, J. H. Davenport, W. M. Farmer, J. Urban, and F. Rabe, Eds., vol. 6824. Springer, 2011. http://dx.doi.org/10.1007/978-3-642-22673-1_11 pp. 149–163.
  7. M. Wenzel, L. C. Paulson, and T. Nipkow, “The Isabelle framework,” in Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, ser. LNCS, O. A. Mohamed, C. A. Muñoz, and S. Tahar, Eds., vol. 5170. Springer, 2008. http://dx.doi.org/10.1007/978-3-540-71067-7_7 pp. 33–38.
  8. J. C. Blanchette, M. Haslbeck, D. Matichuk, and T. Nipkow, “Mining the Archive of Formal Proofs,” in Intelligent Computer Mathematics (CICM 2015), ser. LNCS, M. Kerber, J. Carette, C. Kaliszyk, F. Rabe, and V. Sorge, Eds., vol. 9150. Springer, 2015. http://dx.doi.org/10.1007/978-3-319-20615-8_1 pp. 3–17.
  9. Y. Bertot, “A Short Presentation of Coq,” in Theorem Proving in Higher Order Logics (TPHOLs 2008), ser. LNCS, O. A. Mohamed, C. A. Muñoz, and S. Tahar, Eds., vol. 5170. Springer, 2008. http://dx.doi.org/10.1007/978-3-540-71067-7_3 pp. 12–16.
  10. L. Cruz-Filipe, H. Geuvers, and F. Wiedijk, “C-CoRN, the Constructive Coq Repository at Nijmegen,” in Mathematical Knowledge Management (MKM’04), ser. LNCS, A. Asperti, G. Bancerek, and A. Trybulec, Eds., vol. 3119. Springer, 2004. http://dx.doi.org/10.1007/978-3-540-27818-4_7 pp. 88–103.
  11. G. Gonthier and A. Mahboubi, “An introduction to small scale reflection in Coq,” J. Formalized Reasoning, vol. 3, no. 2, pp. 95–152, 2010. http://dx.doi.org/10.6092/issn.1972-5787/1979
  12. A. Grabowski and T. Mitsuishi, “Formalizing Lattice-Theoretical Aspects of Rough and Fuzzy Sets,” in Rough Sets and Knowledge Technology – 10th International Conference, RSKT 2015, held as part of the International Joint Conference on Rough Sets, IJCRS 2015, Tianjin, China, November 20–23, 2015, Proceedings, 2015. http://dx.doi.org/10.1007/978-3-319-25754-9_31 pp. 347–356.
  13. L. C. Paulson, “Isabelle: The next 700 theorem provers,” in Logic and Computer Science (1990), P. Odifreddi, Ed., 1990, pp. 361–386.
  14. C. Kaliszyk, K. Pąk, and J. Urban, “Towards a Mizar Environment for Isabelle: Foundations and Language,” in Proc. 5th Conference on Certified Programs and Proofs (CPP 2016), J. Avigad and A. Chlipala, Eds. ACM, 2016. http://dx.doi.org/10.1145/2854065.2854070 pp. 58–65.
  15. C. Kaliszyk and K. Pąk, “Presentation and Manipulation of Mizar Properties in an Isabelle Object Logic,” in Intelligent Computer Mathematics - 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings, ser. LNCS, H. Geuvers, M. England, O. Hasan, F. Rabe, and O. Teschke, Eds., vol. 10383. Springer, 2017. http://dx.doi.org/10.1007/978-3-319-62075-6_14 pp. 193–207.
  16. C. Schürmann, “The Twelf Proof Assistant,” in Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, ser. LNCS, S. Berghofer, T. Nipkow, C. Urban, and M. Wenzel, Eds., vol. 5674. Springer, 2009. http://dx.doi.org/10.1007/978-3-642-03359-9_7 pp. 79–83.
  17. F. Rabe, “A logical framework combining model and proof theory,” Mathematical Structures in Computer Science, vol. 23, no. 5, pp. 945–1001, 2013. http://dx.doi.org/10.1017/S0960129512000424
  18. M. Wenzel, “Isar - A Generic Interpretative Approach to Readable Formal Proof Documents,” in Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs’99, ser. LNCS, Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Théry, Eds., vol. 1690. Springer, 1999. http://dx.doi.org/10.1007/3-540-48256-3_12 pp. 167–184.
  19. M. Wenzel and F. Wiedijk, “A Comparison of Mizar and Isar,” J. Autom. Reasoning, vol. 29, no. 3-4, pp. 389–411, 2002. http://dx.doi.org/10.1023/A:1021935419355
  20. K. Pąk, “Readable Formalization of Euler’s Partition Theorem in Mizar,” in Intelligent Computer Mathematics – International Conference, CICM 2015, Washington, DC, USA, July 13–17, 2015, Proceedings, 2015. http://dx.doi.org/10.1007/978-3-319-20615-8_14 pp. 211–226.
  21. K. Pąk, “Automated Improving of Proof Legibility in the Mizar System,” in Intelligent Computer Mathematics – International Conference, CICM 2014, Coimbra, Portugal, July 7–11, 2014. Proceedings, 2014. http://dx.doi.org/10.1007/978-3-319-08434-3_27 pp. 373–387.
  22. K. Pąk, “Improving Legibility of Formal Proofs Based on the Close Reference Principle is NP-hard,” Journal of Automated Reasoning, vol. 55, no. 3, pp. 295–306, 2015. http://dx.doi.org/10.1007/s10817-015-9337-1
  23. J. Harrison, “A Mizar Mode for HOL,” in Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs’96, ser. LNCS, J. von Wright, J. Grundy, and J. Harrison, Eds., vol. 1125. Springer, 1996. http://dx.doi.org/10.1007/BFb0105406 pp. 203–220.
  24. C. Kaliszyk and F. Wiedijk, “Merging Procedural and Declarative Proof,” in Types for Proofs and Programs, International Conference, TYPES 2008, ser. LNCS, S. Berardi, F. Damiani, and U. de’Liguoro, Eds., vol. 5497. Springer, 2008. http://dx.doi.org/10.1007/978-3-642-02444-3_13 pp. 203–219.
  25. D. Syme, “Three Tactic Theorem Proving,” in Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs’99, Nice, France, September, 1999, Proceedings, ser. LNCS, Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin-Mohring, and L. Théry, Eds., vol. 1690. Springer, 1999. http://dx.doi.org/10.1007/3-540-48256-3_14 pp. 203–220.
  26. F. Wiedijk, “Mizar Light for HOL Light,” in Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, ser. LNCS, R. J. Boulton and P. B. Jackson, Eds., vol. 2152. Springer, 2001. doi: 10.1007/3-540-44755-5_26. ISBN 3-540-42525-X pp. 378–394.
  27. F. Wiedijk, “A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving,” Logical Methods in Computer Science, vol. 8, no. 1, 2012. http://dx.doi.org/10.2168/LMCS-8(1:30)2012
  28. P. Corbineau, “A Declarative Language for the Coq Proof Assistant,” in Types for Proofs and Programs, International Conference, TYPES 2007, ser. LNCS, M. Miculan, I. Scagnetto, and F. Honsell, Eds., vol. 4941. Springer, 2007. http://dx.doi.org/10.1007/978-3-540-68103-8_5. ISBN 978-3-540-68084-0 pp. 69–84.
  29. S. Jaśkowski, “On the rules of suppositions,” Studia Logica, vol. 1, 1934.
  30. J. Urban, “MPTP 0.2: Design, implementation, and initial experiments,” J. Autom. Reasoning, vol. 37, no. 1–2, pp. 21–43, 2006. http://dx.doi.org/10.1007/s10817-006-9032-3
  31. C. Kaliszyk and J. Urban, “MizAR 40 for Mizar 40,” J. Autom. Reasoning, vol. 55, no. 3, pp. 245–256, 2015. http://dx.doi.org/10.1007/s10817-015-9330-8
  32. O. Kunčar, “Reconstruction of the Mizar type system in the HOL Light system,” in WDS Proceedings of Contributed Papers: Part I – Mathematics and Computer Sciences, J. Pavlu and J. Safrankova, Eds. Matfyzpress, 2010, pp. 7–12.
  33. A. Grabowski, A. Korniłowicz, and A. Naumowicz, “Mizar in a Nutshell,” J. Formalized Reasoning, vol. 3, no. 2, pp. 153–245, 2010. http://dx.doi.org/10.6092/issn.1972-5787/1980
  34. M. Iancu, M. Kohlhase, F. Rabe, and J. Urban, “The Mizar Mathematical Library in OMDoc: Translation and applications,” J. Autom. Reasoning, vol. 50, no. 2, pp. 191–202, 2013. http://dx.doi.org/10.1007/s10817-012-9271-4
  35. L. C. Paulson, “Set theory for verification: I. From foundations to functions,” J. Autom. Reasoning, vol. 11, no. 3, pp. 353–389, 1993. http://dx.doi.org/10.1007/BF00881873
  36. A. Grabowski, A. Korniłowicz, and A. Naumowicz, “Four Decades of Mizar,” Journal of Automated Reasoning, vol. 55, no. 3, pp. 191–198, October 2015. http://dx.doi.org/10.1007/s10817-015-9345-1
  37. A. Grabowski, A. Korniłowicz, and C. Schwarzweller, “On Algebraic Hierarchies in Mathematical Repository of Mizar,” in Proc. Federated Conference on Computer Science and Information Systems (FedCSIS 2016), M. Ganzha, L. A. Maciaszek, and M. Paprzycki, Eds., 2016. http://dx.doi.org/10.15439/2016F520 pp. 363–371.
  38. A. Grabowski, A. Korniłowicz, and C. Schwarzweller, “Equality in Computer Proof-Assistants,” in Proceedings of the 2015 Federated Conference on Computer Science and Information Systems, ser. Annals of Computer Science and Information Systems, M. Ganzha, L. A. Maciaszek, and M. Paprzycki, Eds., vol. 5. IEEE, 2015. http://dx.doi.org/10.15439/2015F229 pp. 45–54.
  39. A. Korniłowicz, “Definitional expansions in Mizar,” Journal of Automated Reasoning, vol. 55, no. 3, pp. 257–268, October 2015. http://dx.doi.org/10.1007/s10817-015-9331-7. [Online]. Available: http://dx.doi.org/10.1007/s10817-015-9331-7
  40. T. Gauthier and C. Kaliszyk, “Matching concepts across HOL libraries,” in Proc. of the 7th Conference on Intelligent Computer Mathematics (CICM’14), ser. LNCS, S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban, Eds., vol. 8543. Springer, 2014. http://dx.doi.org/10.1007/978-3-319-08434-3_20 pp. 267–281.
  41. C. Kaliszyk and J. Urban, “Learning-assisted Theorem Proving with Millions of Lemmas,” Journal of Symbolic Computation, vol. 69, pp. 109–128, 2015. http://dx.doi.org/10.1016/j.jsc.2014.09.032
  42. P. Corbineau and C. Kaliszyk, “Cooperative Repositories for Formal Proofs,” in Towards Mechanized Mathematical Assistants, 14th Symposium, Calculemus 2007, 6th International Conference, MKM 2007, Hagenberg, Austria, June 27-30, 2007, Proceedings, ser. LNCS, M. Kauers, M. Kerber, R. Miner, and W. Windsteiger, Eds., vol. 4573. Springer, 2007. http://dx.doi.org/10.1007/978-3-540-73086-6_19 pp. 221–234.