Theoretical and Practical Issues in Automated Deduction

关于设计完整而有效的一阶等式理论的定理证明方法的问题将被研究。两种新的证明技术-证明排序和超限语义树-基于简化排序的范例，用于建立各种定理证明方法的完备性，包括分解的精化、参数调整(没有函数自反性公理)和Knuth-Bendex类型方法。一般而言，这些元级别技术形成了严格处理基于重写的等式推理和使用诸如简化(解调)等删除规则的定理证明策略的基础。这些技术将被进一步改进和细化，以将它们应用于更大的问题领域，并为快速制作定理证明者的原型建立一个编程环境。这个定理证明环境将为有效地描述推理规则和搜索计划以及观察和控制证明者的运行环境提供便利。它将包括高效编码的版本和基本运算，如统一、匹配和归约，以及不同的内置抽象定理证明机。正在研究的抽象机的两个特例是用于简化和规范化的归约机和用于基于堆栈的策略的线性抽象机。

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.