License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2019.35
URN: urn:nbn:de:0030-drops-110903
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/11090/
Go to the corresponding LIPIcs Volume Portal

Kaliszyk, Cezary ; Pak, Karol

Declarative Proof Translation (Short Paper)

pdf-format:
LIPIcs-ITP-2019-35.pdf (0.5 MB)

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.

BibTeX - Entry

@InProceedings{kaliszyk_et_al:LIPIcs:2019:11090,
  author =	{Cezary Kaliszyk and Karol Pak},
  title =	{{Declarative Proof Translation (Short Paper)}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{35:1--35:7},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{John Harrison and John O'Leary and Andrew Tolmach},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/11090},
  URN =		{urn:nbn:de:0030-drops-110903},
  doi =		{10.4230/LIPIcs.ITP.2019.35},
  annote =	{Keywords: Declarative Proof, Translation, Isabelle/Isar, Mizar}
}

Keywords: Declarative Proof, Translation, Isabelle/Isar, Mizar
Collection: 10th International Conference on Interactive Theorem Proving (ITP 2019)
Issue Date: 2019
Date of publication: 05.09.2019
Supplementary Material: The translated formalization is available at: {http://cl-informatik.uibk.ac.at/cek/itp19mml200/}

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI