面向形式化证明档案库的 Isabelle 技术及其在 MMT 中的应用
计算机科学中的逻辑
2019-06-12 v2
摘要
本文概述了形式化证明档案库（AFP）背后的 Isabelle 技术。交互式开发与准交互式构建任务对逻辑（通常为 Isabelle/HOL）、用于数学工具实现的 Isabelle/ML 以及用于物理系统集成的 Isabelle/Scala 都提出了显著的可扩展性需求——它们均集成于 Isabelle/PIDE（证明器 IDE）中。AFP 的持续增长要求 Isabelle 性能不断改进。本文报告了 Isabelle2019（2019 年 6 月）中的现状，以及诸如证明器会话导出和基于语义信息实现自动更新的无头 PIDE 等值得注意的附加功能。一个示例应用是 Isabelle/MMT，它能够将整个 Isabelle + AFP 转换为 OMDoc 与 RDF 三元组，但复用该 Isabelle 技术用于其他应用是直截了当的。
引用
@article{arxiv.1905.07244,
title = {Isabelle technology for the Archive of Formal Proofs with application to MMT},
author = {Makarius Wenzel},
journal= {arXiv preprint arXiv:1905.07244},
year = {2019}
}