文章基本信息

标题：Declarative Proof Translation (Short Paper)
本地全文：下载
作者：Cezary Kaliszyk ; Karol Pak
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2019
卷号：141
页码：1-7
DOI：10.4230/LIPIcs.ITP.2019.35
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：Declarative Proof; Translation; Isabelle/Isar; Mizar