CD Tools——基于凝聚 detachment 与结构生成的定理证明（系统描述）
计算机科学中的逻辑
2022-07-19 v1 人工智能
摘要
CD Tools是一个Prolog库，用于在一阶ATP中实验凝聚detachment（condensed detachment），将近期以证明结构为核心的正式观点付诸实践。从一阶ATP的视角看，凝聚detachment提供了一种相对简单但具备本质特征和严肃应用的设定，使其成为开发和评估新技术的有吸引力的基础。CD Tools包含基于证明结构枚举的专用证明器。我们在此聚焦于其中之一SGCD，它允许以特别灵活的方式混合目标驱动与公理驱动的证明搜索。在纯目标驱动配置下，它的行为类似于子句表格或连接方法族的证明器。在混合配置下，其性能强得多，接近SOTA证明器，同时给出较短的证明。实验展示了该证明器所实现的结构生成方法的特征与应用可能。对于一个ATP中常被研究的历史问题，它给出了比任何已知证明都短得多的新证明。
引用
@article{arxiv.2207.08453,
title = {CD Tools -- Condensed Detachment and Structure Generating Theorem Proving (System Description)},
author = {Christoph Wernhard},
journal= {arXiv preprint arXiv:2207.08453},
year = {2022}
}