论文标题
使Isabelle内容以知识表示格式访问
Making Isabelle Content Accessible in Knowledge Representation Formats
论文作者
论文摘要
众所周知，像Isabelle，Coq，Hol这样的证明助手的图书馆很难用外部工具来解释：事实上，只有供者本身才能充分解析和处理它们。就Isabelle而言，该图书馆将图书馆的出口到公平（可访问，可互操作和可重复使用的）知识交换格式已在1999年被设想，但以前证明太困难了。从那以后，经过iSabelle Prover IDE（PIDE）和OMDOC/MMT格式的大量改进后，我们现在能够提供这样的出口。具体而言，我们提出了PIDE和MMT的集成，该集成允许以OMDOC格式导出所有Isabelle库。我们的出口涵盖了完整的Isabelle分布和正式证明的档案（AFP） - 超过65GB的OMDOC/XML超过65GB。 Isabelle内容的系统导出到OMDOC（例如OMDOC）等定义明确的互换格式，可以实现许多应用程序，例如依赖关系管理，独立的证明检查或库搜索。
The libraries of proof assistants like Isabelle, Coq, HOL are notoriously difficult to interpret by external tools: de facto, only the prover itself can parse and process them adequately. In the case of Isabelle, an export of the library into a FAIR (Findable, Accessible, Interoperable, and Reusable) knowledge exchange format was already envisioned by the authors in 1999 but had previously proved too difficult. After substantial improvements of the Isabelle Prover IDE (PIDE) and the OMDoc/Mmt format since then, we are now able to deliver such an export. Concretely we present an integration of PIDE and MMT that allows exporting all Isabelle libraries in OMDoc format. Our export covers the full Isabelle distribution and the Archive of Formal Proofs (AFP) -- more than 12 thousand theories and locales resulting in over 65GB of OMDoc/XML. Such a systematic export of Isabelle content to a well-defined interchange format like OMDoc enables many applications such as dependency management, independent proof checking, or library search.
