Presentation and Manipulation of Mizar Properties in an Isabelle Object Logic

Cezary Kaliszyk and Karol Pąk

10th International Conference on Intelligent Computer Mathematics, LNCS 10383, pp. 193-207, 2017..


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.


  PDF |    doi:10.1007/978-3-319-62075-6_14  


author = {Cezary Kaliszyk and Karol Pak},
title = {Presentation and Manipulation of {M}izar Properties in an {I}sabelle Object Logic},
pages = {193--207},
doi = {10.1007/978-3-319-62075-6_14},
booktitle = {10th International Conference on Intelligent Computer Mathematics (CICM'17)},
year = {2017},
editor = {Herman Geuvers and Matthew England and Osman Hasan and Florian Rabe and Olaf Teschke},
series = {LNCS},
volume = {10383},
publisher = {Springer},
Nach oben scrollen