Skip to main content
SpringerLink
Log in

Isabelle Import Infrastructure for the Mizar Mathematical Library

  • Conference paper
  • First Online:
Intelligent Computer Mathematics (CICM 2018)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 11006))

Included in the following conference series:

Abstract

We present an infrastructure that allows importing an initial part of the Mizar Mathematical Library into the Isabelle/Mizar object logic. For this, we first combine the syntactic information provided by the Mizar parser with the syntactic one originating from the Mizar verifier. The proof outlines are then imported by an Isabelle package, that translates particular Mizar directives to appropriate Isabelle meta-logic constructions. This includes processing of definitions, notations, typing information, and the actual theorem statements, so far without proofs. To show that the imported 100 articles give rise to a usable Isabelle environment, we use the environment to formalize proofs in the Isabelle/Mizar environment using the imported types and their properties.

The paper has been supported by the resources of the Polish National Science Center granted by decision n\(^\circ \)DEC-2015/19/D/ST6/01473.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    These rarely affect the HTMLization of the current Mizar library, see for example http://mizar.uwb.edu.pl/version/current/html/funct_2.html#FC4 where the expression includes rather than . Note the reverse order or arguments.

References

  1. Alama, J., Kohlhase, M., Mamane, L., Naumowicz, A., Rudnicki, P., Urban, J.: Licensing the Mizar mathematical library. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) CICM 2011. LNCS (LNAI), vol. 6824, pp. 149–163. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22673-1_11

    Chapter  Google Scholar 

  2. Aspinall, D., Kaliszyk, C.: What’s in a theorem name? In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 459–465. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-43144-4_28

    Chapter  MATH  Google Scholar 

  3. Bancerek, G., et al.: Mizar: State-of-the-art and beyond. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS (LNAI), vol. 9150, pp. 261–279. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-20615-8_17

    Chapter  Google Scholar 

  4. Bancerek, G., Urban, J.: Integrated semantic browsing of the Mizar mathematical library for authoring Mizar articles. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 44–57. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27818-4_4

    Chapter  MATH  Google Scholar 

  5. Blanchette, J.C., Greenaway, D., Kaliszyk, C., Kühlwein, D., Urban, J.: A learning-based fact selector for Isabelle/HOL. J. Autom. Reason. 57(3), 219–244 (2016). https://doi.org/10.1007/s10817-016-9362-8

    Article  MathSciNet  MATH  Google Scholar 

  6. Brown, C.E., Urban, J.: Extracting higher-order goals from the Mizar mathematical library. In: Kohlhase, M., Johansson, M., Miller, B., de de Moura, L., Tompa, F. (eds.) CICM 2016. LNCS (LNAI), vol. 9791, pp. 99–114. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-42547-4_8

    Chapter  Google Scholar 

  7. Bylinski, C., Alama, J.: New developments in parsing Mizar. In: Jeuring, J., et al. (eds.) CICM 2012. LNCS (LNAI), vol. 7362, pp. 427–431. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31374-5_30

    Chapter  Google Scholar 

  8. Corbineau, P., Kaliszyk, C.: Cooperative repositories for formal proofs. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) Calculemus/MKM -2007. LNCS (LNAI), vol. 4573, pp. 221–234. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73086-6_19

    Chapter  Google Scholar 

  9. Gauthier, T., Kaliszyk, C.: Sharing HOL4 and HOL light proof knowledge. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 372–386. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-48899-7_26

    Chapter  MATH  Google Scholar 

  10. Grabowski, A., Korniłowicz, A., Naumowicz, A.: Four decades of Mizar. J. Autom. Reason. 55(3), 191–198 (2015)

    Article  MathSciNet  Google Scholar 

  11. Hurd, J.: The OpenTheory standard theory library. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 177–191. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20398-5_14

    Chapter  Google Scholar 

  12. Iancu, M., Kohlhase, M., Rabe, F., Urban, J.: The Mizar mathematical library in OMDoc: translation and applications. J. Autom. Reason. 50(2), 191–202 (2013)

    Article  MathSciNet  Google Scholar 

  13. Irving, G., Szegedy, C., Alemi, A.A., Eén, N., Chollet, F., Urban, J.: DeepMath - deep sequence models for premise selection. In: Lee, D.D., Sugiyama, M., von Luxburg, U., Guyon, I., Garnett, R. (eds.) NIPS, pp. 2235–2243 (2016)

    Google Scholar 

  14. Kaliszyk, C., Krauss, A.: Scalable LCF-style proof translation. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 51–66. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39634-2_7

    Chapter  Google Scholar 

  15. Kaliszyk, C., Pąk, K.: Semantics of Mizar as an Isabelle object logic (submitted). http://cl-informatik.uibk.ac.at/cek/submitted/ckkp-jar17.pdf

  16. Kaliszyk, C., Pąk, K.: Presentation and manipulation of Mizar properties in an Isabelle object logic. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds.) CICM 2017. LNCS (LNAI), vol. 10383, pp. 193–207. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-62075-6_14

    Chapter  Google Scholar 

  17. Kaliszyk, C., Pąk, K.: Progress in the independent certification of Mizar mathematical library in Isabelle. In: Ganzha, M., Maciaszek, L.A., Paprzycki, M. (eds.) Proceedings of the 2017 Federated Conference on Computer Science and Information Systems, FedCSIS 2017, pp. 227–236 (2017)

    Google Scholar 

  18. Kaliszyk, C., Pąk, K., Urban, J.: Towards a Mizar environment for Isabelle: foundations and language. In: Avigad, J., Chlipala, A. (eds.) Proceedings of the 5th Conference on Certified Programs and Proofs (CPP 2016), pp. 58–65. ACM (2016)

    Google Scholar 

  19. Kaliszyk, C., Urban, J.: Learning-assisted theorem proving with millions of lemmas. J. Symb. Comput. 69, 109–128 (2015)

    Article  MathSciNet  Google Scholar 

  20. Kaliszyk, C., Urban, J.: MizAR 40 for Mizar 40. J. Autom. Reason. 55(3), 245–256 (2015)

    Article  MathSciNet  Google Scholar 

  21. Naumowicz, A., Piliszek, R.: Accessing the Mizar library with a weakly strict Mizar parser. In: Kohlhase, M., Johansson, M., Miller, B., de Moura, L., Tompa, F. (eds.) CICM 2016. LNCS (LNAI), vol. 9791, pp. 77–82. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-42547-4_6

    Chapter  Google Scholar 

  22. Obua, S., Skalberg, S.: Importing HOL into Isabelle/HOL. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 298–302. Springer, Heidelberg (2006). https://doi.org/10.1007/11814771_27

    Chapter  Google Scholar 

  23. Pąk, K.: Combining the syntactic and semantic representations of Mizar proofs (submitted)

    Google Scholar 

  24. Urban, J.: XML-izing Mizar: making semantic processing and presentation of MML easy. In: Kohlhase, M. (ed.) MKM 2005. LNCS (LNAI), vol. 3863, pp. 346–360. Springer, Heidelberg (2006). https://doi.org/10.1007/11618027_23

    Chapter  Google Scholar 

  25. Urban, J.: MPTP 0.2: design, implementation, and initial experiments. J. Autom. Reason. 37(1–2), 21–43 (2006)

    MATH  Google Scholar 

  26. Urban, J., Bancerek, G.: Presenting and explaining Mizar. Electr. Notes Theor. Comput. Sci. 174(2), 63–74 (2007)

    Article  Google Scholar 

  27. Urban, J., Sutcliffe, G.: ATP-based cross-verification of Mizar proofs: method, systems, and first experiments. Math. Comput. Sci. 2(2), 231–251 (2008)

    Article  MathSciNet  Google Scholar 

  28. Wenzel, M.: Isabelle as document-oriented proof assistant. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) CICM 2011. LNCS (LNAI), vol. 6824, pp. 244–259. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22673-1_17

    Chapter  Google Scholar 

  29. Wenzel, M., Paulson, L.C., Nipkow, T.: The Isabelle framework. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 33–38. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71067-7_7

    Chapter  Google Scholar 

  30. Wenzel, M., Wiedijk, F.: A comparison of Mizar and Isar. J. Autom. Reason. 29(3–4), 389–411 (2002)

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Universität Innsbruck, Innsbruck, Austria

    Cezary Kaliszyk

  2. Uniwersytet w Białymstoku, Białystok, Poland

    Karol Pąk

Authors
  1. Cezary Kaliszyk
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Karol Pąk
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Cezary Kaliszyk .

Editor information

Editors and Affiliations

  1. Department of Computer Science, Friedrich-Alexander-Universität Erlangen-Nürnberg, Erlangen, Bayern, Germany

    Florian Rabe

  2. Department of Computing and Software, McMaster University, Hamilton, Ontario, Canada

    William M. Farmer

  3. University of Cambridge, Cambridge, United Kingdom

    Grant O. Passmore

  4. Department of Computer Science, The George Washington University, Washington, District of Columbia, USA

    Abdou Youssef

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Kaliszyk, C., Pąk, K. (2018). Isabelle Import Infrastructure for the Mizar Mathematical Library. In: Rabe, F., Farmer, W., Passmore, G., Youssef, A. (eds) Intelligent Computer Mathematics. CICM 2018. Lecture Notes in Computer Science(), vol 11006. Springer, Cham. https://doi.org/10.1007/978-3-319-96812-4_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-96812-4_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-96811-7

  • Online ISBN: 978-3-319-96812-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation