Logo PTI
Polish Information Processing Society
Logo FedCSIS

Annals of Computer Science and Information Systems, Volume 15

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

Combining the Syntactic and Semantic Representations of Mizar Proofs

DOI: http://dx.doi.org/10.15439/2018F248

Citation: Proceedings of the 2018 Federated Conference on Computer Science and Information Systems, M. Ganzha, L. Maciaszek, M. Paprzycki (eds). ACSIS, Vol. 15, pages 145–153 ()

Full text

Abstract. The Mizar system provides two representations of the proofs present in its library. The syntactic representation preserves the human-friendly rich Mizar language, where the meaning of structures and expressions is still influenced by their context. The semantic one, on the other hand, explicitly reflects the meaning of all elements present in the proof scripts, however many features of the Mizar language are eliminated.

References

  1. G. Bancerek, C. Byliński, 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.
  2. G. Bancerek, C. Byliński, A. Grabowski, A. Korniłowicz, R. Matuszewski, A. Naumowicz, and K. Pąk, “The role of the Mizar Mathematical Library for interactive proof development in Mizar,” Journal of Automated Reasoning, 2017. http://dx.doi.org/10.1007/s10817-017-9440-6. [Online]. Available: https://doi.org/10.1007/s10817-017-9440-6
  3. G. Bancerek and P. Rudnicki, “Information retrieval in MML,” in Mathematical Knowledge Management, MKM 2003, ser. LNCS, A. Asperti, B. Buchberger, and J. H. Davenport, Eds., vol. 2594. Springer, 2003. http://dx.doi.org/10.1007/3-540-36469-2_10. ISBN 3-540-00568-4 pp. 119–132. [Online]. Available: https://doi.org/10.1007/3-540-36469-2_10
  4. J. Urban, “XML-izing Mizar: Making semantic processing and presentation of MML easy,” in Mathematical Knowledge Management (MKM 2005), ser. LNCS, M. Kohlhase, Ed., vol. 3863. Springer, 2005. ISBN 3-540-31430-X pp. 346–360.
  5. 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
  6. 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
  7. 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
  8. A. Naumowicz and R. Piliszek, “Accessing the Mizar library with a weakly strict Mizar parser,” in Intelligent Computer Mathematics, CICM 2016, ser. LNCS, M. Kohlhase, M. Johansson, B. R. Miller, L. de Moura, and F. W. Tompa, Eds., vol. 9791. Springer, 2016. http://dx.doi.org/10.1007/978-3-319-42547-4_6 pp. 77–82. [Online]. Available: http://doi.org/10.1007/978-3-319-42547-4_6
  9. C. Byliński and J. Alama, “New Developments in Parsing Mizar,” in Intelligent Computer Mathematics - 11th International Conference, AISC 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, DML 2012, 11th International Conference, MKM 2012, Systems and Projects, Held as Part of CICM 2012, ser. 7362, J. Jeuring, J. A. Campbell, J. Carette, G. D. Reis, P. Sojka, M. Wenzel, and V. Sorge, Eds., vol. 5170. Springer, 2012. http://dx.doi.org/10.1007/978-3-642-31374-5 pp. 427–431.
  10. J. Urban, “Translating Mizar for first order theorem provers,” in Mathematical Knowledge Management, Second International Conference, MKM 2003, Bertinoro, Italy, February 16-18, 2003, Proceedings, ser. LNCS, A. Asperti, B. Buchberger, and J. H. Davenport, Eds., vol. 2594. Springer, 2003. http://dx.doi.org/10.1007/3-540-36469-2_16 pp. 203–215.
  11. J. Urban and G. Sutcliffe, “ATP-based cross-verification of Mizar proofs: Method, systems, and first experiments,” Math. in Computer Science, vol. 2, no. 2, pp. 231–251, 2008. http://dx.doi.org/10.1007/s11786-008-0053-7
  12. 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.
  13. C. E. Brown and J. Urban, “Extracting higher-order goals from the Mizar Mathematical Library,” in Intelligent Computer Mathematics (CICM 2016), ser. LNCS, M. Kohlhase, M. Johansson, B. R. Miller, L. de Moura, and F. W. Tompa, Eds., vol. 9791. Springer, 2016. http://dx.doi.org/10.1007/978-3-319-42547-4_8 pp. 99–114.
  14. J. Urban, P. Rudnicki, and G. Sutcliffe, “ATP and presentation service for Mizar formalizations,” J. Autom. Reasoning, vol. 50, no. 2, pp. 229–241, 2013. http://dx.doi.org/10.1007/s10817-012-9269-y. [Online]. Available: https://doi.org/10.1007/s10817-012-9269-y
  15. J. C. Blanchette, D. Greenaway, C. Kaliszyk, D. Kühlwein, and J. Urban, “A learning-based fact selector for Isabelle/HOL,” J. Autom. Reasoning, vol. 57, no. 3, pp. 219–244, 2016. http://dx.doi.org/10.1007/s10817-016-9362-8. [Online]. Available: http://dx.doi.org/10.1007/s10817-016-9362-8
  16. 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.
  17. 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. doi: 10.1145/2854065.2854070 pp. 58–65.
  18. C. Kaliszyk and K. Pąk, “Progress in the independent certification of Mizar Mathematical Library in Isabelle,” in Proceedings of the 2017 Federated Conference on Computer Science and In- formation Systems, FedCSIS 2017, M. Ganzha, L. A. Maciaszek, and M. Paprzycki, Eds., 2017. http://dx.doi.org/10.15439/2017F289 pp. 227– 236.
  19. C. Kaliszyk and K. Pąk, “Isabelle formalization of set theoretic structures and set comprehensions,” in Mathematical Aspects of Computer and Information Sciences, MACIS 2017, ser. LNCS, J. Blamer, T. Kutsia, and D. Simos, Eds., vol. 10693. Springer, 2017. http://dx.doi.org/10.1007/978-3-319-72453-9_12 pp. 227–236.
  20. 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
  21. 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
  22. S. Jaśkowski, “On the rules of suppositions,” Studia Logica, vol. 1, 1934.
  23. J. Urban and G. Sutcliffe, “ATP cross-verification of the Mizar MPTP challenge problems,” in Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference, LPAR 2007, Yerevan, Armenia, October 15–19, 2007, Proceedings, 2007. http://dx.doi.org/10.1007/978-3-540-75560-9_39 pp. 546–560.
  24. K. Pąk, “Methods of lemma extraction in natural deduction proofs,” Journal of Automated Reasoning, vol. 50, no. 2, pp. 217–228, February 2013. http://dx.doi.org/10.1007/s10817-012-9267-0. [Online]. Available: http://dx.doi.org/10.1007/s10817-012-9267-0
  25. C. Kaliszyk and K. Pąk, “Semantics of Mizar as an Isabelle object logic,” accepted by Journal of Automated Reasoning, http://cl-informatik.uibk.ac.at/cek/submitted/ckkp-jar17.pdf.