Alignment-based Translations Across Formal Systems Using Interface Theories
Alignment-based Translations Across Formal Systems Using Interface Theories
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, …