Alignment-based Translations Across Formal Systems Using Interface Theories

Dennis Müller
(Computer Science, FAU Erlangen-Nürnberg)
Colin Rothgang
(Mathematics, Jacobs University Bremen)
Yufei Liu
(Mathematics, Jacobs University Bremen)
Florian Rabe
(Computer Science, Jacobs University Bremen)

Translating expressions between different logics and theorem provers is notoriously and often prohibitively difficult, due to the large differences between the logical foundations, the implementations of the systems, and the structure of the respective libraries. Practical solutions for exchanging theorems across theorem provers have remained both weak and brittle. Consequently, libraries are not easily reusable across systems, and substantial effort must be spent on reformalizing and proving basic results in each system. Notably, this problem exists already if we only try to exchange theorem statements and forgo exchanging proofs.

In previous work we introduced alignments as a lightweight standard for relating concepts across libraries and conjectured that it would provide a good base for translating expressions. In this paper, we demonstrate the feasibility of this approach. We use a foundationally uncommitted framework to write interface theories that abstract from logical foundation, implementation, and library structure. Then we use alignments to record how the concepts in the interface theories are realized in several major proof assistant libraries, and we use that information to translate expressions across libraries. Concretely, we present exemplary interface theories for several areas of mathematics and - in total - several hundred alignments that were found manually.

In Catherine Dubois and Bruno Woltzenlogel Paleo: Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving (PxTP 2017), Brasília, Brazil, 23-24 September 2017, Electronic Proceedings in Theoretical Computer Science 262, pp. 77–93.
Published: 4th December 2017.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: