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.

BibTeX

@inproceedings{ckkp-cicm18,
  author    = {Cezary Kaliszyk and Karol P\k{a}k},
  title     = {Isabelle Import Infrastructure for the {M}izar Mathematical Library},
  booktitle = {11th International Conference on Intelligent Computer Mathematics (CICM 2018)},
  pages     = {131--146},
  year      = {2018},
  url       = {https://doi.org/10.1007/978-3-319-96812-4\_13},
  doi       = {10.1007/978-3-319-96812-4\_13},
  editor    = {Florian Rabe and
               William M. Farmer and
               Grant O. Passmore and
               Abdou Youssef},
  series    = {LNCS},
  volume    = {11006},
  publisher = {Springer},
}