Isabelle Import Infrastructure for the Mizar Mathematical Library

Cezary Kaliszyk and Karol Pąk

11th International Conference on Intelligent Computer Mathematics, LNCS 11006, pp. 131 – 146, 2018..


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.


  PDF |    doi:10.1007/978-3-319-96812-4_13 |  © Springer International Publishing AG, part of Springer Nature 2018


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 = {\_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},
Nach oben scrollen