Instance-Based Theorem Proving with Semantics and Equality

一阶逻辑是表示数学和其他形式知识的常见形式主义。 在计算机上证明一阶定理的许多传统技术在某些类型的问题（如近似命题的高度非Horn问题）上效率低下。 根据以前的赠款，定理证明策略已经开发出来，避免了许多这些命题效率低下。这些包括超链接和超链接与语义。 后一种方法能够利用问题的现实模型或语义。 然而，它可以使用的模型的种类仅限于那些涉及线性不等式和那些有限域。 这种方法现在将被扩展到包括一个更一般的模型类，那些函数和谓词是可计算的。 具有相等性的一阶逻辑是一种更强大的形式主义，也经常适用。 对于这种形式主义，基于术语重写系统的方法通常被应用。 上述语义技术将被推广到一阶逻辑等式。 与平等有关的其他主题也将进行研究，如严格的E统一和专门的算法，用于处理从方程系统产生的排列。 一个一般的框架-最近开发的研究搜索效率的定理证明策略，并在很大程度上应用于命题的上下文中-将扩展到一阶逻辑。 还将研究与项重写证明相关的复杂性问题。 ***

First-order logic is a common formalism for representing mathematical and other formal knowledge. Many traditional techniques for proving first-order theorems on a computer suffer from severe inefficiencies on certain kinds of problems such as near-propositional highly non-Horn problems. Under previous grants, theorem proving strategies have been developed that avoid many of these propositional inefficiencies. These include hyper- linking and hyper-linking with semantics. The latter method is able to make use of realistic models, or semantics, of the problem. However, the kinds of models it can use are limited to those involving linear inequalities and those with finite domains. This approach will now be extended to include a much more general class of models, those whose functions and predicates are computable. First-order logic with equality is a more powerful formalism that is also often applicable. For this formalism, methods based on term-rewriting systems are commonly applied. The above-mentioned semantic techniques will be extended to first-order logic with equality. Other topics related to equality will also be studied, such as rigid E-unification and specialized algorithms for handling permutations that arise from equational systems. A general framework---recently developed for studying the search efficiency of theorem proving strategies, and applied in a largely propositional context---will be extended to first-order logic. Complexity issues related to term-rewriting proofs will also be studied. ***