LIPIcs.ITP.2023.37.pdf
- Filesize: 0.68 MB
- 8 pages
Document
Implementing More Explicit Definitional Expansions in Mizar (Short Paper)
Authors
Adam Grabowski 
,
Artur Korniłowicz
-
Part of:
Volume:
14th International Conference on Interactive Theorem Proving (ITP 2023)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-07-26
File
Document Identifiers
Author Details
Acknowledgements
The authors are grateful to the reviewers for their constructive comments. The Mizar processing has been performed using the infrastructure of the University of Białystok High Performance Computing Center.
Cite As Get BibTex
Adam Grabowski and Artur Korniłowicz. Implementing More Explicit Definitional Expansions in Mizar (Short Paper). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 37:1-37:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ITP.2023.37
Abstract
The Mizar language and its corresponding proof-checker offers the tactic of definitional expansions in proof skeletons. This apparatus is rather fragile in the case of intensive overloading of notions (which is widely observed e.g. in the field of algebra, but it is also present in the more fundamental set-theory contexts). We propose the extension of this mechanism: the change should offer users the more precise control over expansions via choosing the right definitional variant for the proof under consideration, still letting the authors to retain the more conservative approach. As a rule, the change will affect new Mizar texts, but obviously, it allows also for solving some context conflicts caused by the original approach in the Mizar repository. The usefulness of our approach is shown by a number of experiments carried out within MML, which is also affected by the change.
Subject Classification
ACM Subject Classification
- Theory of computation → Interactive proof systems
Keywords
- Mizar
- definitions
- proof assistants
- mechanization of proof
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
Supplementary Materials
-
Dataset (test files)
https://github.com/arturkornilowicz/unfolding
browse
archived version
References
- 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 Proceedings, volume 9150 of LNCS, pages 261-279. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-20615-8_17.
- 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.
- Czesław Byliński, Artur Korniłowicz, and Adam Naumowicz. Syntactic-semantic form of Mizar articles. In Liron Cohen and Cezary Kaliszyk, editors, 12th International Conference on Interactive Theorem Proving (ITP 2021), volume 193 of Leibniz International Proceedings in Informatics (LIPIcs), pages 11:1-11:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.11.
- Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Mizar in a nutshell. Journal of Formalized Reasoning, Special Issue: User Tutorials I, 3(2):153-245, 2010. URL: https://doi.org/10.6092/issn.1972-5787/1980.
- Adam Grabowski, Artur Korniłowicz, and Christoph Schwarzweller. Equality in computer proof-assistants. In Maria Ganzha, Leszek A. Maciaszek, and Marcin Paprzycki, editors, Proceedings of the 2015 Federated Conference on Computer Science and Information Systems, volume 5 of Annals of Computer Science and Information Systems, pages 45-54. IEEE, 2015. URL: https://doi.org/10.15439/2015F229.
- 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 Proceedings, volume 11006 of LNCS, pages 131-146. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-96812-4_13.
- Cezary Kaliszyk and Karol Pąk. Declarative proof translation (short paper). In John Harrison, John O'Leary, and Andrew Tolmach, editors, 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA, volume 141 of LIPIcs, pages 35:1-35:7. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.ITP.2019.35.
- Artur Korniłowicz. Definitional expansions in Mizar. Journal of Automated Reasoning, 55(3):257-268, October 2015. URL: https://doi.org/10.1007/s10817-015-9331-7.
- Adam Naumowicz. Tools for MML environment analysis. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics - International Conference, CICM 2015 Proceedings, volume 9150 of LNCS, pages 348-352. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-20615-8_26.
- 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, volume 15 of Annals of Computer Science and Information Systems, pages 145-153. IEEE, 2018. URL: https://doi.org/10.15439/2018F248.
- Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9-11, 1990. URL: http://fm.mizar.org/1990-1/pdf1-1/tarski.pdf.
- Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, and Josef Urban. Exploration of neural machine translation in autoformalization of mathematics in Mizar. In Jasmin Blanchette and Catalin Hritcu, editors, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pages 85-98, 2020. URL: https://doi.org/10.1145/3372885.3373827.
- Makarius Wenzel. The Isabelle/Isar Reference Manual, 2021. URL: https://isabelle.in.tum.de/doc/isar-ref.pdf.
- Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73-83, 1990. URL: http://fm.mizar.org/1990-1/pdf1-1/relat_1.pdf.