Abstract
One of the crucial factors enabling an efficient use of a logical framework is the convenience of entering, manipulating, and presenting object logic constants, statements, and proofs. In this paper, we discuss various elements of the Mizar language and the possible ways how these can be represented in the Isabelle framework in order to allow a suitable way of working in typed set theory. We explain the interpretation of various components declared in each Mizar article environment and create Isabelle attributes and outer syntax that allow simulating them. We further discuss introducing notations for symbols defined in the Mizar Mathematical Library, but also synonyms and redefinitions of such symbols. We also compare the language elements corresponding to the actual proofs, with special care for implicit proof expansions not present in Isabelle. We finally discuss Mizar’s hidden arguments and demonstrate that some of them are not necessary in an Isabelle representation.
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.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
Trueprop is the HOL object logic constant that turns a higher-order logic boolean into a meta-level proposition.
References
Abrial, J., Butler, M.J., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. STTT 12(6), 447–466 (2010)
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, vol. 6824, pp. 149–163. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22673-1_11
Bancerek, G.: On the structure of Mizar types. In: Geuvers, H., Kamareddine, F. (eds.) ENTCS, vol. 85, pp. 69–85. Elsevier (2003)
Bancerek, G., Byliński, C., Grabowski, A., Korniłowicz, A., Matuszewski, R., Naumowicz, A., Pa̧k, K., Urban, J.: Mizar: state-of-the-art and beyond. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS, vol. 9150, pp. 261–279. Springer, Cham (2015). doi:10.1007/978-3-319-20615-8_17
Grabowski, A., Korniłowicz, A., Naumowicz, A.: Four decades of Mizar. J. Autom. Reasoning 55(3), 191–198 (2015)
Kaliszyk, C., Pąk, K., Urban, J.: Towards a Mizar environment for Isabelle: foundations and language. In: Avigad, J., Chlipala, A. (eds.) Conference on Certified Programs and Proofs (CPP 2016), pp. 58–65. ACM (2016). doi:10.1145/2854065.2854070
Kaliszyk, C., Urban, J.: MizAR 40 for Mizar 40. J. Autom. Reasoning 55(3), 245–256 (2015). doi:10.1007/s10817-015-9330-8
Korniłowicz, A.: On rewriting rules in Mizar. J. Autom. Reasoning 50(2), 203–210 (2013)
Korniłowicz, A.: Enhancement of Mizar texts with transitivity property of predicates. In: Kohlhase, M., Johansson, M., Miller, B., de Moura, L., Tompa, F. (eds.) CICM 2016. LNCS, vol. 9791, pp. 157–162. Springer, Cham (2016). doi:10.1007/978-3-319-42547-4_12
Megill, N.D.: Metamath: A Computer Language for Pure Mathematics. Lulu Press, Morrisville, North Carolina (2007)
Obua, S., Fleuriot, J.D., Scott, P., Aspinall, D.: ProofPeer: Collaborative theorem proving. CoRR, abs/1404.6186 (2014)
Obua, S., Fleuriot, J., Scott, P., Aspinall, D.: Type inference for ZFH. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS, vol. 9150, pp. 87–101. Springer, Cham (2015). doi:10.1007/978-3-319-20615-8_6
Paulson, L.C.: Isabelle: the next 700 theorem provers. In: Odifreddi, P. (ed.) Logic and Computer Science (1990), pp. 361–386 (1990)
Paulson, L.C.: Set theory for verification: I. From foundations to functions. J. Autom. Reasoning 11(3), 353–389 (1993)
Pąk, K.: Improving legibility of formal proofs based on the close reference principle is NP-hard. J. Autom. Reasoning 55(3), 295–306 (2015)
Rabe, F.: A logical framework combining model and proof theory. Math. Struct. Comput. Sci. 23(5), 945–1001 (2013)
Schürmann, C.: The Twelf proof assistant. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 79–83. Springer, Heidelberg (2009). doi:10.1007/978-3-642-03359-9_7
Urban, J., Sutcliffe, G.: ATP-based cross-verification of Mizar proofs: method, systems, and first experiments. Math. in Comput. Sci. 2(2), 231–251 (2008)
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). doi:10.1007/978-3-540-71067-7_7
Wiedijk, F. (ed.): The Seventeen Provers of the World. LNCS (LNAI), vol. 3600. Springer, Heidelberg (2006). doi:10.1007/11542384
Acknowledgements
We thank Chad Brown for the discussions on the various set-theoretic foundations. This work has been supported by the ERC grant no. 714034 SMART and OeAD Scientific & Technological Cooperation with Poland grant PL 03/2016.
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Kaliszyk, C., Pąk, K. (2017). Presentation and Manipulation of Mizar Properties in an Isabelle Object Logic. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds) Intelligent Computer Mathematics. CICM 2017. Lecture Notes in Computer Science(), vol 10383. Springer, Cham. https://doi.org/10.1007/978-3-319-62075-6_14
Download citation
DOI: https://doi.org/10.1007/978-3-319-62075-6_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-62074-9
Online ISBN: 978-3-319-62075-6
eBook Packages: Computer ScienceComputer Science (R0)