论文标题
CD工具 - 凝结的分离和结构生成定理证明（系统描述）
CD Tools -- Condensed Detachment and Structure Generating Theorem Proving (System Description)
论文作者
论文摘要
CD工具是一个序言库，用于试验一阶ATP中的凝结脱离，这将围绕证明结构的最新正式视图付诸实践。从一阶ATP的角度来看，凝结的支队提供了一个相对简单但具有重要功能和严肃应用的设置，使其成为开发和评估新技术的基础的吸引力。 CD工具包括基于证明结构的列举的专业抛弃。我们将重点放在其中一种SGCD上，该SGCD允许以特别灵活的方式将目标和Axiom驱动的证明搜索融合。在纯粹的目标驱动配置中，它的作用类似于Clausal Tableaux或Connection方法家族的鄙视。在混合配置中，其性能要强得多，靠近最先进的掠夺，同时发出相对较短的证据。实验显示了该供者实现的结构生成方法的特征和应用可能性。对于经常在ATP中研究的历史性问题，它产生了一种比任何已知的证据要短得多。
CD Tools is a Prolog library for experimenting with condensed detachment in first-order ATP, which puts a recent formal view centered around proof structures into practice. From the viewpoint of first-order ATP, condensed detachment offers a setting that is relatively simple but with essential features and serious applications, making it attractive as a basis for developing and evaluating novel techniques. CD Tools includes specialized provers based on the enumeration of proof structures. We focus here on one of these, SGCD, which permits to blend goal- and axiom-driven proof search in particularly flexible ways. In purely goal-driven configurations it acts similarly to a prover of the clausal tableaux or connection method family. In blended configurations its performance is much stronger, close to state-of-the-art provers, while emitting relatively short proofs. Experiments show characteristics and application possibilities of the structure generating approach realized by that prover. For a historic problem often studied in ATP it produced a new proof that is much shorter than any known one.
