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 out 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

@inproceedings{ckkp-itp19,
  author    = {Cezary Kaliszyk and Karol Pąk},
  title     = {Declarative Proof Translation (short paper)},
  booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)},
  year      = {2019},
  series    = {LIPIcs},
  pages     = {35:1--35:7},
  url       = {https://doi.org/10.4230/LIPIcs.ITP.2019.35},
  doi       = {10.4230/LIPIcs.ITP.2019.35},
  editor    = {John Harrison and John O'Leary and Andrew Tolmach},
  volume    = {141},
}