A New Export of the Mizar Mathematical Library
Rothgang C, Korniłowicz A, Rabe F (2021)
Publication Type: Conference contribution
Publication year: 2021
Journal
Publisher: Springer Science and Business Media Deutschland GmbH
Book Volume: 12833 LNAI
Pages Range: 205-210
Conference Proceedings Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Event location: Virtual, Online
ISBN: 9783030810962
DOI: 10.1007/978-3-030-81097-9_17
Abstract
The Mizar Mathematical Library (MML) is a prime target of library exports, i.e., translations of proof assistant libraries that make the libraries available to knowledge management systems or other deduction systems. The MML has been exported multiple times in the past, including our own export from Mizar to OMDoc done in 2011. But the exporters tend to be very difficult and expensive to maintain. We present a complete reimplementation of our previous export. It incorporates many lessons learned and leverages improvements made both on the Mizar and the OMDoc side.
Authors with CRIS profile
Involved external institutions
Germany (DE)How to cite
APA:
Rothgang, C., Korniłowicz, A., & Rabe, F. (2021). A New Export of the Mizar Mathematical Library. In Fairouz Kamareddine, Claudio Sacerdoti Coen (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 205-210). Virtual, Online: Springer Science and Business Media Deutschland GmbH.
MLA:
Rothgang, Colin, Artur Korniłowicz, and Florian Rabe. "A New Export of the Mizar Mathematical Library." Proceedings of the 14th International Conference on Intelligent Computer Mathematics, CICM 2021, Virtual, Online Ed. Fairouz Kamareddine, Claudio Sacerdoti Coen, Springer Science and Business Media Deutschland GmbH, 2021. 205-210.
BibTeX: Download