RIA: The Theory of General Unification and Rigid E-Unification

统一算法构成了几乎所有自动演绎系统的核心，将基本范式推广到具有等式的一阶逻辑和高阶逻辑，促使了更一般形式的统一的设计。这份报告建议用赫布兰德发明的术语系统转换的方法，继续国际社会发展一般统一理论的工作。还在研究第一个已知的通用电子统一算法的开发，以及实现高阶统一的新技术。此外，还将研究安德鲁的匹配方法的扩展，以解释平等，其中涉及一种称为刚性E-统一的新形式的统一。

Unification algorithms form the core of almost all automated deduction systems, and generalizations of the basic paradigms to first-order logic with equality and to higher-order logic have motivated the design of more general forms of unification. This report proposes to continue the PI's work in developing a theory of general unification using the method of transformation on systems of terms invented by Herbrand. Also under investigation is the development of the first known algorithm for general E-unification and new techniques for implementing higher-order unification. In addition, an extension of Andrew's method of matings to account for equality, which involves a new form of unification called rigid E-unification will be studied.