Experiences from Exporting Major Proof Assistant Libraries
Experiences from Exporting Major Proof Assistant Libraries
复制标题
出口主要证明辅助库的经验
DOI：
--
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Florian Rabe
中科院分区：
文献类型：
--
作者：
M. Kohlhase;Florian Rabe
证明助手的互操作性及其图书馆的整合是在定理证明领域的高度重视但难以捉摸的目标。作为预备步骤，在先前的工作中，我们将多个证明助手的库，特别是Coq，hol Light，Imps，Isabelle，Mizar和PVS的库中：OMDOC/MMT。每次翻译都呈现出巨大的理论，技术和社会挑战，有些是普遍的，有些是特定于系统的，有些可以解决，有些仍然开放。在本文中，我们调查了这些挑战，并比较和评估我们选择的解决方案。我们认为，类似的图书馆翻译将是任何未来系统互操作性解决方案的重要组成部分，我们的经验将对他人进行此类努力很有价值。
The interoperability of proof assistants and the integration of their libraries is a highly valued but elusive goal in the field of theorem proving. As a preparatory step, in previous work, we translated the libraries of multiple proof assistants, specifically the ones of Coq, HOL Light, IMPS, Isabelle, Mizar, and PVS into a universal format: OMDoc/MMT. Each translation presented great theoretical, technical, and social challenges, some universal and some system-specific, some solvable and some still open. In this paper, we survey these challenges and compare and evaluate the solutions we chose. We believe similar library translations will be an essential part of any future system interoperability solution, and our experiences will prove valuable to others undertaking such efforts.