Logo PTI
Polish Information Processing Society
Logo FedCSIS

Annals of Computer Science and Information Systems, Volume 17

Communication Papers of the 2018 Federated Conference on Computer Science and Information Systems

Mizar Set Comprehension in Isabelle Framework

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

Citation: Communication Papers of the 2018 Federated Conference on Computer Science and Information Systems, M. Ganzha, L. Maciaszek, M. Paprzycki (eds). ACSIS, Vol. 17, pages 23–26 ()

Full text

Abstract. The Mizar project from its beginning aimed to make a highly human oriented proof environment where the proof style closely reflects the informal proofs style. The support is reflected in the size of the largest consistent formal library\mbox{\,---\,}Mizar Mathematical Library (MML). However, the Mizar system is the only tool that provides full verification and further development of the MML. In this paper, we present the progress in the development of the Isabelle/Mizar project whose main goal is independent cross-verification of the MML in Isabelle. We focus on Mizar set comprehension operators that allow defining sets that satisfy a given predicate. The development already covers simple cases where the arity of predicates is limited to two. We propose an infrastructure that provides a more elegant and recursive approach to construct and to provide the main property of set comprehension operators.

References

  1. 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
  2. K. Pąk, “Topological manifolds,” Formalized Mathematics, vol. 22, no. 2, pp. 179–186, 2014. http://dx.doi.org/10.2478/forma-2014-0019
  3. G. Bancerek and P. Rudnicki, “A Compendium of Continuous Lattices in MIZAR,” J. Autom. Reasoning, vol. 29, no. 3–4, pp. 189–224, 2002.
  4. 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
  5. 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.
  6. 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
  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. Grabowski, A. Korniłowicz, and A. Naumowicz, “Four decades of Mizar,” Journal of Automated Reasoning, vol. 55, no. 3, pp. 191–198, 2015. http://dx.doi.org/10.1007/s10817-015-9345-1
  9. 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
  10. 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.
  11. 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.
  12. 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 Information Systems, FedCSIS 2017, M. Ganzha, L. A. Maciaszek, and M. Paprzycki, Eds., 2017. http://dx.doi.org/10.15439/2017F289 pp. 227–236.
  13. L. C. Paulson and J. C. Blanchette, “Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers,” in Workshop on the Implementation of Logics, IWIL 2010, ser. EPiC Series, G. Sutcliffe, S. Schulz, and E. Ternovska, Eds., vol. 2. EasyChair, 2010, pp. 1–11.
  14. 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, pp. 163–178.
  15. J. Urban, “MPTP - motivation, implementation, first experiments,” J. Autom. Reasoning, vol. 33, no. 3-4, pp. 319–339, 2004. http://dx.doi.org/10.1007/s10817-004-6245-1. [Online]. Available: https://doi.org/10. 1007/s10817-004-6245-1
  16. 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.
  17. C. Kaliszyk and K. Pąk, “Presentation and manipulation of Mizar properties in an Isabelle object logic,” in Intelligent Computer Mathematics - CICM 2017, 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.
  18. 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