Saturation-Based Theorem Proving

在自动定理证明中，有两种演算比较流行：饱和演算、表演算和连接演算。 后者支持目标导向的证明搜索，但前者是上级的逻辑与平等和类似的领域。 定理证明中最引人注目的成就-Robbins问题的解是用饱和方法得到的。在基于饱和的演绎中，冗余是一个关键概念。 如果公式或推论对矛盾的任何推导都没有贡献，或者以允许替代但更简单的推导的方式做出贡献，则它们是多余的。 如果一个集合的所有推论都是冗余的，则该集合称为饱和的，并且只有当存在明确的矛盾时才是不一致的。 因此，饱和为检查不一致性提供了基础。 通过将结论添加到当前公式集，推理总是可以变得冗余，但是出于效率原因，避免生成冗余公式的技术是必不可少的。 本项目的目标是进一步深入了解这一过程，并通过关注三个关键技术-饱和、扩展和组合来推进定理证明技术。近似是指分别针对无变量公式和一般公式连接不同级别的推理的技术，如统一和约束。 饱和证明器的性能通常取决于近似和冗余技术之间的微妙相互作用。通过新符号对形式语言的扩展在自动演绎中有不同的用途，例如，在同余闭包算法中。 本研究的目的是发展一个理论的同余闭包饱和为基础的决策程序，不仅包括标准的同余闭包，但也扩展到更丰富的理论和消除方法翻译回originallanguage.Saturation技术已隐含地用于计算机代数方法，如Buchberger的算法或吴的方法证明定理的几何。 该计划是重新制定这些方法在逻辑方面，以便将它们集成在通用的证明和应用定理证明技术，以获得优化或扩展的决策程序。

Two kinds of calculi are prevalent in automated theorem proving: saturation calculi and tableau and connection calculi. The latter support a goal-directed proof search, but the former are superior for logics with equality and similar domains. The most spectacular success for theorem proving to date---the solution of the Robbins problem was obtained with a saturation method.In saturation-based deduction, redundancy is a key concept. Formulas or inferences are redundant if they either do not contribute to any derivation of a contradiction, or else contribute in ways that allow for alternative, but simpler derivations. If all inferences from a set are redundant, the set is called saturated and is inconsistent only if there is an explicit contradiction. Saturation thus provides a basis for checking for inconsistency. An inference can always be rendered redundant by adding its conclusion to the current set of formulas, but techniques that avoid the generation of redundant formulas are indispensable for efficiency reasons. The objectives of this project are to develop further insights into this process and to advance theorem proving technology by focusing on three key technique---saturation, extension, and combination.Approximation refers to techniques such as unification and constraints that connect inferences at different levels, for variable-free and general formulas, respectively. The performance of saturation provers often depends on the subtle interaction between approximation and redundancy techniques. The extension of a formal language by new symbols has different uses in automated deduction, e.g., in congruence closure algorithms. This research aims at developing a theory of congruence closure as saturation-based decision procedures, to include not only standard congruence closure, but also extensions to richer theories and elimination methods for translating back to the original language.Saturation techniques have been implicitly used in computer algebra methods such as Buchberger's algorithm or Wu's method for proving theorems in geometry. The plan is to reformulate these methods in logical terms so as to integrate them in general-purpose provers and apply theorem proving techniques to obtain optimized or extended decision procedures.