Saturation-Based Theorem Proving

基于饱和的定理证明

• 批准号: 9902031
• 负责人: Leo Bachmair
• 金额: $ 19.84万
• 依托单位: SUNY at Stony Brook
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1999
• 资助国家: 美国
• 起止时间: 1999-09-01 至 2003-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9902031&HistoricalAwards=false
• 关键词: Saturation; Based; Theorem; Proving

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.

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