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.

BibTeX

@inproceedings{ckkp-cicm17,
 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},
}