Theoretical and Practical Issues in Automated Deduction

自动演绎的理论与实践问题

• 批准号: 8901322
• 负责人: Leo Bachmair
• 金额: $ 11.24万
• 依托单位: SUNY at Stony Brook
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1989
• 资助国家: 美国
• 起止时间: 1989-06-01 至 1992-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=8901322&HistoricalAwards=false
• 关键词: Theoretical; Practical; Issues; Automated; Deduction

Issues regarding the design of complete, yet efficient, theorem proving methods for first-order theories with equality will be studied. Two new proof techniques-proof orderings and transfinite semantic trees- based on the paradigm of simplification orderings and used to establish the completeness of a variety of theorem proving methods, including refinements of resolution, paramodulation (without the functional reflexivity axioms), and Knuth-Bendix type methods. These meta-level techniques form the basis for a rigorous treatment of rewrite-based equational reasoning and of theorem proving strategies with deletion rules such as simplification (demodulation), in general. These techniques will be further refined and elaborated to apply them to larger problem domains, and to build a programming environment for quickly prototyping theorem provers. This theorem proving environment will provide facilities for effectively describing inference rules and search plans, and observing and controlling the run-time environment of provers. It will include efficiently coded versions and primitive operations such as unification, matching and reduction, as well as different built-in abstract theorem-proving machines. Two special cases of abstract machines being studied are a reduction machine for simplification and normalization, and a linear abstract machine for stack-based strategies.

将研究有关设计完整且有效的一阶理论等式定理证明方法的问题。 两种新的证明技术——证明排序和超限语义树——基于简化排序范式，用于建立各种定理证明方法的完整性，包括解析的细化、副调制（没有函数自反性公理）和 Knuth-Bendix 类型的方法。 一般来说，这些元级技术构成了严格处理基于重写的等式推理和具有删除规则（例如简化（解调））的定理证明策略的基础。 这些技术将被进一步细化和阐述，以将其应用于更大的问题领域，并构建用于快速原型定理证明者的编程环境。 该定理证明环境将为有效描述推理规则和搜索计划以及观察和控制证明者的运行时环境提供设施。 它将包括有效编码的版本和原始操作，例如统一、匹配和约简，以及不同的内置抽象定理证明机。 正在研究的抽象机的两个特殊情况是用于简化和规范化的归约机，以及用于基于堆栈的策略的线性抽象机。