The Mizar Mathematical Library in OMDoc: Translation and Applications

• Published in: Journal of automated reasoning 2013-02, Vol.50 (2), p.191-202
• Main Authors: Iancu, Mihnea, Kohlhase, Michael, Rabe, Florian, Urban, Josef
• Format: Article
• Language: English
• Subjects: Artificial Intelligence; Computer Science; Mathematical Logic and Formal Languages; Mathematical Logic and Foundations; Symbolic and Algebraic Manipulation
• ISSN: 0168-7433; 1573-0670
• DOI: 10.1007/s10817-012-9271-4

The Mizar Mathematical Library is one of the largest libraries of formalized and mechanically verified mathematics. Its language is highly optimized for authoring by humans. As in natural languages, the meaning of an expression is influenced by its (mathematical) context in a way that is natural to humans, but harder to specify for machine manipulation. Thus its custom file format can make the access to the library difficult. Indeed, the Mizar system itself is currently the only system that can fully operate on the Mizar library. This paper presents a translation of the Mizar library into the OMDoc format ( O pen M athematical Doc uments), an XML-based representation format for mathematical knowledge. OMDoc is geared towards machine support and interoperability by making formula structure and context dependencies explicit. Thus, the Mizar library becomes accessible for a wide range of OMDoc-based tools for formal mathematics and knowledge management. We exemplify interoperability by indexing the translated library in the M ath W eb S earch engine, which provides an “applicable theorem search” service (almost) out of the box.