Saturation-Based Theorem Proving

自动化定理证明中常用的两种演算：饱和演算、表演算和连接演算。后者支持目标导向的证明搜索，但前者更适合具有相等和相似域的逻辑。迄今为止最引人注目的定理证明成功——用饱和法得到了罗宾斯问题的解。在基于饱和的演绎中，冗余是一个关键概念。公式或推论是多余的，如果它们要么不能对矛盾的任何推导作出贡献，要么以其他方式作出贡献，但更简单的推导。如果来自一个集合的所有推理都是冗余的，则该集合称为饱和的，只有当存在显式矛盾时，该集合才是不一致的。因此，饱和度为检查不一致提供了基础。通过将结论添加到当前的一组公式中，推理总是可以变得冗余，但是出于效率原因，避免生成冗余公式的技术是必不可少的。本项目的目标是进一步深入了解这一过程，并通过关注三个关键技术——饱和、扩展和组合来推进定理证明技术。近似指的是诸如统一和约束等技术，它们分别用于无变量公式和一般公式，将不同层次的推论联系起来。饱和证明的性能往往取决于近似和冗余技术之间微妙的相互作用。用新符号扩展形式语言在自动演绎中有不同的用途，例如在同余闭包算法中。本研究旨在发展一种基于饱和的决策过程的同余闭包理论，该理论不仅包括标准的同余闭包，而且还扩展到更丰富的理论和消除方法，用于翻译回原语言。饱和技术已被隐式地用于计算机代数方法，如Buchberger算法或Wu的几何定理证明方法。计划是用逻辑术语重新表述这些方法，以便将它们整合到通用证明程序中，并应用定理证明技术来获得优化或扩展的决策过程。

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.