HOL Light 与 TPTP 的认证连接表证明
计算机科学中的逻辑
2014-10-22 v1 人工智能
摘要
近年来，基于有序参数化归结和模型消除的 Metis 证明器已取代 HOL4 和 Isabelle/HOL 中早期的内置通用证明自动化方法。然而，在年度 CASC 竞赛中，基于连接表 (connection tableaux) 的 leanCoP 系统表现优于 Metis。本文展示了如何在 HOL Light 内部实现 leanCoP 的核心算法。leanCoP 的标志性特征即其极简核心，造就了一个非常简单的证明系统。这在将 MESON 证明重构机制扩展至连接表证明中起到了关键作用，从而提供了一种能够认证其证明的 leanCoP 实现。我们讨论了使用显式 Prolog 堆栈的直接实现与 HOL Light 中现有的 MESON 续体传递实现之间的差异，并在所有核心 HOL Light 目标上比较了它们的性能。生成的证明器也可用作通用的 TPTP 证明器。我们在 TPTP 及其他有趣数据集上将其性能与基于归结的 Metis 进行了比较。
引用
@article{arxiv.1410.5476,
title = {Certified Connection Tableaux Proofs for HOL Light and TPTP},
author = {Cezary Kaliszyk and Josef Urban and Jiri Vyskocil},
journal= {arXiv preprint arXiv:1410.5476},
year = {2014}
}