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.
翻译:CD 工具是一个用于试验一级 ATP 中精密分解的Prolog 库, 它使最近围绕证据结构的正式视图成为实践。 从第一级 ATP 的角度来看, 精密分解提供了相对简单但具有基本特征和认真应用的设置, 使得它具有开发和评价新技术的吸引力。 CD 工具包括基于列举证据结构的专门证明。 我们在此集中关注其中之一, SGCD, 它允许以特别灵活的方式混合目标- 和xiom 驱动的校对搜索。 它在纯粹由目标驱动的配置中, 与光线形平板或连接法家族的验证者类似。 在混合配置中, 它的性能更强, 接近于最先进的验证者, 同时提供相对较短的证明。 实验显示了该验证者所实现的结构的特性和应用可能性。 对于在ATP 中经常研究的一个历史问题, 它产生的新证据比已知的要短得多。