LIPIcs.ITP.2019.35.pdf
- Filesize: 0.51 MB
- 7 pages
Document
Declarative Proof Translation (Short Paper)
Authors
Cezary Kaliszyk 
,
Karol Pąk
-
Part of:
Volume:
10th International Conference on Interactive Theorem Proving (ITP 2019)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2019-09-05
File
Document Identifiers
Author Details
Cite AsGet BibTex
Cezary Kaliszyk and Karol Pąk. Declarative Proof Translation (Short Paper). In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 35:1-35:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ITP.2019.35
https://doi.org/10.4230/LIPIcs.ITP.2019.35
Abstract
Declarative proof styles of different proof assistants include a number of incompatible features. In this paper we discuss and classify the differences between them and propose efficient algorithms for declarative proof outline translation. We demonstrate the practicality of our algorithms by automatically translating the proof outlines in 200 articles from the Mizar Mathematical Library to the Isabelle/Isar proof style. This generates the corresponding theories with 15301 proof outlines accepted by the Isabelle proof checker. The goal of our translation is to produce a declarative proof in the target system that is both accepted and short and therefore readable. For this three kinds of adaptations are required. First, the proof structure often needs to be rebuilt to capture the extensions of the natural deduction rules supported by the systems. Second, the references to previous items and their labels need to be matched and aligned. Finally, adaptations in the annotations of individual proof step may be necessary.
Subject Classification
ACM Subject Classification
- Theory of computation → Interactive proof systems
Keywords
- Declarative Proof
- Translation
- Isabelle/Isar
- Mizar
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Mark Adams. Proof Auditing Formalised Mathematics. J. Formalized Reasoning, 9(1):3-32, 2016. URL: https://jfr.unibo.it/article/view/4576.
- 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, 2017. URL: https://doi.org/10.1007/s10817-017-9440-6.
- Pierre Corbineau. A Declarative Language for the Coq Proof Assistant. In Marino Miculan, Ivan Scagnetto, and Furio Honsell, editors, Types for Proofs and Programs, International Conference, TYPES 2007, volume 4941 of LNCS, pages 69-84. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-68103-8_5.
- Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean Theorem Prover (System Description). In Amy P. Felty and Aart Middeldorp, editors, Conference on Automated Deduction, CADE 2015, volume 9195 of LNCS, pages 378-388. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21401-6_26.
- Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four Decades of Mizar. Journal of Automated Reasoning, 55(3):191-198, 2015. URL: https://doi.org/10.1007/s10817-015-9345-1.
- John Harrison. A Mizar Mode for HOL. In Joakim von Wright, Jim Grundy, and John Harrison, editors, Theorem Proving in Higher Order Logics: TPHOLs 1996, volume 1125 of LNCS, pages 203-220. Springer, 1996. URL: https://doi.org/10.1007/BFb0105406.
- 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, 11th International Conference on Intelligent Computer Mathematics (CICM 2018), 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. Semantics of Mizar as an Isabelle Object Logic. Journal of Automated Reasoning, 2018. URL: https://doi.org/10.1007/s10817-018-9479-z.
- Markus Wenzel and Freek Wiedijk. A Comparison of Mizar and Isar. J. Autom. Reasoning, 29(3-4):389-411, 2002. URL: https://doi.org/10.1023/A:1021935419355.
- Freek Wiedijk. Mizar Light for HOL Light. In Richard J. Boulton and Paul B. Jackson, editors, Theorem Proving in Higher Order Logics, TPHOLs 2001, volume 2152 of LNCS, pages 378-394. Springer, 2001. URL: https://doi.org/10.1007/3-540-44755-5_26.
- Freek Wiedijk. A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving. Logical Methods in Computer Science, 8(1), 2012. URL: https://doi.org/10.2168/LMCS-8(1:30)2012.