将 HOL Light 证明转换为 Metamath

Mario Carneiro

将 HOL Light 证明转换为 Metamath

计算机科学中的逻辑 2015-06-22 v2 逻辑

作者: Mario Carneiro

摘要

我们提出了一种算法，用于将来自 OpenTheory 交换格式的证明转换为基于 ZFC 的 Metamath 语言，该格式可与 HOL 家族的任意证明语言（HOL4、HOL Light、ProofPower 和 Isabelle）相互翻译。该任务分为两步：首先将 OpenTheory 证明翻译为 Metamath HOL 形式化文件 $\mathtt{\text{hol.mm}}$ ，随后将 HOL 形式化嵌入到 Metamath 主库 $\mathtt{\text{set.mm}}$ 的主要 ZFC 基础中。这一过程提供了一种手段，将 Metamath 基础的简洁性与 HOL Light 中产生成果的强力自动化努力联系起来，从而能够生成 HOL Light 定理的完整 Metamath 证明，同时也证明了相对于 Metamath 的 ZFC 公理化体系，HOL Light 是一致的。

关键词

证明转换 HOL Light Metamath OpenTheory ZFC 基础形式化验证定理证明

引用

@article{arxiv.1412.8091,
  title  = {Conversion of HOL Light proofs into Metamath},
  author = {Mario Carneiro},
  journal= {arXiv preprint arXiv:1412.8091},
  year   = {2015}
}

备注

14 pages, 2 figures, accepted to Journal of Formalized Reasoning

将 HOL Light 证明转换为 Metamath

摘要

关键词

引用

备注

相关论文