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

RIA：普遍统一理论和严格电子统一理论

• 批准号: 8910268
• 负责人: Wayne Snyder
• 金额: --
• 依托单位: Trustees of Boston University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1989
• 资助国家: 美国
• 起止时间: 1989-09-01 至 1992-02-29
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=8910268&HistoricalAwards=false
• 关键词: RIA; Theory; General; Unification; Rigid

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.

统一算法形成了几乎所有自动演绎系统的核心，并且将基本范式推广到具有等式的一阶逻辑和更高阶逻辑已经激发了更一般形式的统一的设计。本报告建议继续PI的工作，在发展理论的一般统一使用的方法转换系统的条款发明的Herbrand。也正在调查的是第一个已知的算法一般E统一和新技术的发展，实现高阶统一。此外，扩展安德鲁的方法交配占平等，其中涉及一种新的形式的统一称为刚性E-统一将进行研究。