Document Open Access Logo

Declarative Proof Translation (Short Paper)

Authors Cezary Kaliszyk , Karol Pąk

Thumbnail PDF


  • Filesize: 0.51 MB
  • 7 pages

Document Identifiers

Author Details

Cezary Kaliszyk
  • University of Innsbruck, Austria
  • University of Warsaw, Poland
Karol Pąk
  • University of Białystok, Poland

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)


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
  • Declarative Proof
  • Translation
  • Isabelle/Isar
  • Mizar


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail