Document Open Access Logo

Syntactic-Semantic Form of Mizar Articles

Authors Czesław Byliński, Artur Korniłowicz , Adam Naumowicz

PDF
Thumbnail PDF

File

LIPIcs.ITP.2021.11.pdf
  • Filesize: 0.67 MB
  • 17 pages

Document Identifiers

Author Details

Czesław Byliński
  • Computer Networks Section, University of Bialystok, Poland
Artur Korniłowicz
  • Institute of Computer Science, University of Bialystok, Poland
Adam Naumowicz
  • Institute of Computer Science, University of Bialystok, Poland

Acknowledgements

The Mizar processing has been performed using the infrastructure of the University of Bialystok High Performance Computing Center.

Cite AsGet BibTex

Czesław Byliński, Artur Korniłowicz, and Adam Naumowicz. Syntactic-Semantic Form of Mizar Articles. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 11:1-11:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.ITP.2021.11

Abstract

Mizar Mathematical Library is most appreciated for the wealth of mathematical knowledge it contains. However, accessing this publicly available huge corpus of formalized data is not straightforward due to the complexity of the underlying Mizar language, which has been designed to resemble informal mathematical papers. For this reason, most systems exploring the library are based on an internal XML representation format used by semantic modules of Mizar. This representation is easily accessible, but it lacks certain syntactic information available only in the original human-readable Mizar source files. In this paper we propose a new XML-based format which combines both syntactic and semantic data. It is intended to facilitate various applications of the Mizar library requiring fullest possible information to be retrieved from the formalization files.

Subject Classification

ACM Subject Classification
  • Information systems → Extensible Markup Language (XML)
Keywords
  • Mizar system
  • mathematical knowledge representation
  • XML representation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze, and Josef Urban. Premise selection for mathematics by corpus analysis and kernel methods. J. Autom. Reasoning, 52(2):191-213, 2014. URL: https://doi.org/10.1007/s10817-013-9286-5.
  2. Grzegorz Bancerek. Automatic translation in Formalized Mathematics. Mechanized Mathematics and Its Applications, 5(2):19-31, December 2006. Google Scholar
  3. Grzegorz Bancerek. Information retrieval and rendering with MML query. In Jonathan Borwein and William Farmer, editors, Mathematical Knowledge Management, volume 4108 of Lecture Notes in Computer Science, pages 266-279. Springer Berlin Heidelberg, 2006. URL: https://doi.org/10.1007/11812289_21.
  4. Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pąk. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9-32, June 2018. URL: https://doi.org/10.1007/s10817-017-9440-6.
  5. Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings, volume 9150 of Lecture Notes in Computer Science, pages 261-279. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-20615-8_17.
  6. Grzegorz Bancerek, Adam Naumowicz, and Josef Urban. System description: XSL-based translator of Mizar to LaTeX. In Florian Rabe, William M. Farmer, Grant O. Passmore, and Abdou Youssef, editors, Intelligent Computer Mathematics - 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings, volume 11006 of Lecture Notes in Computer Science, pages 1-6. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-96812-4_1.
  7. Czesław Byliński and Jesse Alama. New developments in parsing Mizar. In Johan Jeuring, John A. Campbell, Jacques Carette, Gabriel Dos Reis, Petr Sojka, Makarius Wenzel, and Volker Sorge, editors, Intelligent Computer Mathematics 11th International Conference, AISC 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, DML 2012, 11th International Conference, MKM 2012, Systems and Projects, volume 7362 of Lecture Notes in Artificial Intelligence, pages 427-431. Springer-Verlag, Berlin, Heidelberg, 2012. URL: https://doi.org/10.1007/978-3-642-31374-5_30.
  8. Ingo Dahn. Interpretation of a Mizar-like logic in first-order logic. In Ricardo Caferra and Gernot Salzer, editors, FTP (LNCS Selection), volume 1761 of Lecture Notes in Computer Science, pages 137-151. Springer, 1998. URL: https://doi.org/10.1007/3-540-46508-1_9.
  9. Mihnea Iancu, Michael Kohlhase, Florian Rabe, and Josef Urban. The Mizar Mathematical Library in OMDoc: Translation and applications. Journal of Automated Reasoning, 50(2):191-202, February 2013. URL: https://doi.org/10.1007/s10817-012-9271-4.
  10. Cezary Kaliszyk and Karol Pąk. Isabelle import infrastructure for the Mizar Mathematical Library. In Florian Rabe, William M. Farmer, Grant O. Passmore, and Abdou Youssef, editors, Intelligent Computer Mathematics - 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings, volume 11006 of Lecture Notes in Computer Science, pages 131-146. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-96812-4_13.
  11. Cezary Kaliszyk and Josef Urban. MizAR 40 for Mizar 40. CoRR, abs/1310.2805, 2013. URL: http://arxiv.org/abs/1310.2805.
  12. Roman Matuszewski and Piotr Rudnicki. Mizar: The first 30 years. Mechanized Mathematics and Its Applications, Special Issue on 30 Years of Mizar, 4(1):3-24, March 2005. Google Scholar
  13. Kazuhisa Nakasho. Development of a flexible Mizar tokenizer and parser for information retrieval system. In Maria Ganzha, Leszek A. Maciaszek, and Marcin Paprzycki, editors, Proceedings of the 2019 Federated Conference on Computer Science and Information Systems, FedCSIS 2019, Leipzig, Germany, September 1-4, 2019, volume 18 of Annals of Computer Science and Information Systems, pages 77-80, 2019. URL: https://doi.org/10.15439/2019F151.
  14. Adam Naumowicz and Radosław Piliszek. Accessing the Mizar library with a weakly strict Mizar parser. In Michael Kohlhase, Moa Johansson, Bruce R. Miller, Leonardo de Moura, and Frank Wm. Tompa, editors, Intelligent Computer Mathematics - 9th International Conference, CICM 2016, Bialystok, Poland, July 25-29, 2016, Proceedings, volume 9791 of Lecture Notes in Computer Science, pages 77-82. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-42547-4_6.
  15. Karol Pąk. Combining the Syntactic and Semantic Representations of Mizar Proofs. In Maria Ganzha, Leszek A. Maciaszek, and Marcin Paprzycki, editors, Proceedings of the 2018 Federated Conference on Computer Science and Information Systems, FedCSIS 2018, Poznan, Poland, September 9-12, 2018, volume 15 of Annals of Computer Science and Information Systems, pages 145-153. IEEE, 2018. URL: https://doi.org/10.15439/2018F248.
  16. J. Urban, G. Sutcliffe, S. Trac, and Y. Puzis. Combining Mizar and TPTP Semantic Presentation and Verification Tools. Studies in Logic, Grammar and Rhetoric, 18(31):121-136, 2009. Google Scholar
  17. Josef Urban. XML-izing Mizar: Making semantic processing and presentation of MML easy. In Michael Kohlhase, editor, Mathematical Knowledge Management, 4th International Conference, MKM 2005, Bremen, Germany, July 15-17, 2005, Revised Selected Papers, volume 3863 of Lecture Notes in Computer Science, pages 346-360. Springer, 2005. URL: https://doi.org/10.1007/11618027_23.
  18. Josef Urban. MizarMode - an integrated proof assistance tool for the Mizar way of formalizing mathematics. Journal of Applied Logic, 4(4):414-427, 2006. Google Scholar
  19. Josef Urban. MoMM - fast interreduction and retrieval in large libraries of formalized mathematics. Int. J. on Artificial Intelligence Tools, 15(1):109-130, 2006. URL: http://ktiml.mff.cuni.cz/~urban/MoMM/momm.ps.
  20. Josef Urban, Piotr Rudnicki, and Geoff Sutcliffe. ATP and presentation service for Mizar formalizations. Journal of Automated Reasoning, 50(2):229-241, February 2013. URL: https://doi.org/10.1007/s10817-012-9269-y.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact