以知识表示格式实现Isabelle内容的可访问化
计算机科学中的逻辑
2020-05-19 v1
摘要
诸如Isabelle、Coq、HOL等证明助手的库以难以被外部工具解释而著称：实际上，只有证明器本身能充分解析和处理它们。以Isabelle为例，作者早在1999年便设想将其库导出为FAIR（可发现、可访问、可互操作、可重用）知识交换格式，但此前被认为过于困难。鉴于此后Isabelle Prover IDE（PIDE）与OMDoc/Mmt格式的重大改进，我们如今能够实现此类导出。具体地，我们提出了PIDE与MMT的集成，可将所有Isabelle库以OMDoc格式导出。我们的导出涵盖完整的Isabelle发行版与Archive of Formal Proofs（AFP）——超过1.2万个理论与locale，生成超过65GB的OMDoc/XML。这种将Isabelle内容系统性导出至如OMDoc般定义良好的交换格式，使得诸多应用成为可能，例如依赖管理、独立证明检查或库搜索。
引用
@article{arxiv.2005.08884,
title = {Making Isabelle Content Accessible in Knowledge Representation Formats},
author = {Michael Kohlhase and Florian Rabe and Makarius Wenzel},
journal= {arXiv preprint arXiv:2005.08884},
year = {2020}
}