ProofWatch：E 系统中大理论的手表列表引导
人工智能
2019-05-24 v2 机器学习
计算机科学中的逻辑
摘要
手表列表（亦称提示列表）是一种允许相关证明来引导针对新猜想的证明搜索的机制。该机制已用于 Otter 与 Prover9 定理证明器，既用于交互式形式化，也用于小理论中开放猜想的人工辅助证明。在本工作中，我们探索将手表列表用于来自大型 ITP 库一阶翻译的大理论，旨在通过 ATP 系统更智能的内部引导来改进锤式自动化。具体而言，我们 (i) 在 E ATP 系统内设计基于手表列表的子句评估启发式方法，以及 (ii) 开发新的证明引导算法，这些算法将许多先前的证明载入 ATP 中，并利用动态更新的证明匹配概念聚焦证明搜索。该方法在来自 Mizar 库的大量问题上进行了评估，显示出对 E 的标准策略组合以及先前通过进化方法为 Mizar 发明的最佳策略组合的显著改进。
引用
@article{arxiv.1802.04007,
title = {ProofWatch: Watchlist Guidance for Large Theories in E},
author = {Zarathustra Goertzel and Jan Jakubův and Stephan Schulz and Josef Urban},
journal= {arXiv preprint arXiv:1802.04007},
year = {2019}
}
备注
19 pages, 10 tables, submitted to ITP 2018 at FLOC