Equality Reasoning: Word and Unification Problems

等式推理：词与统一问题

• 批准号: 9712388
• 负责人: Christopher Lynch
• 金额: $ 14.26万
• 依托单位: Clarkson University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1997
• 资助国家: 美国
• 起止时间: 1997-09-01 至 2001-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9712388&HistoricalAwards=false
• 关键词: Equality; Reasoning; Word; Unification; Problems

This project concerns equational reasoning, with emphasis on word and unification problems. The investigation comprises graphs, congruence closure and equational unification, along with further development of these topics, and combinations of these topics. The objective is to develop new decidability and complexity results, and to design and implement efficient algorithms. The approach to word problems will use the rewriting paradigm, concentrating on procedures and data structures for computing complete/canonical sets of rewrite rules. In particular, the method using SOUR graphs for completing rewrite systems will be investigated, particularly the way in which SOUR Graphs can be used to develop procedures for solving the word problem in certain classes of theories. The first part of the research will be to examine the procedure in its simplest form, on string rewriting systems. Once methods are developed to solve the word problem in its simplest form, those methods will be moved back into pure equational logic, and finally into full first order equational logic. For ground equational theories, the plan is to investigate techniques for computing congruence closures based on the rewriting paradigm developed in studying Shostak's congruence closure method. Applications to combinations of decision procedures will be investigated. The relationship between the congruence closure method and SOUR graphs will be investigated and exploited. In unification, the concentration is on semantic unification, where some of the function symbols have semantics associated with them, usually specified in the form of an equational theory. The main focus of the applications is automated reasoning and symbolic computation. E-unification problems arising in process algebra. Knowledge representation and constraint solvers will also be investigated. Both theoretical and practical issues will be studied: (1) on the theoretical side, decidability and complexity issues on variou s equational unification and disunification problems will be investigated---this is a continuation of work done over the past several years; (2) on the practical side, the goal is to come up with efficient algorithms along with fast implementations, making use of heuristics. Implementations will be incorporated into the Unification Workbench, a library of unification algorithms.

该项目涉及方程推理，重点是单词和统一问题。调查包括图形，一致性封闭和方程式统一，以及这些主题的进一步发展以及这些主题的组合。 目的是开发新的可决定性和复杂性结果，并设计和实施有效的算法。 单词问题的方法将使用重写范式，专注于计算重写规则的完整/规范集的过程和数据结构。 特别是，将研究使用酸形图完成重写系统的方法，尤其是可以使用酸形图来开发某些理论类别中解决问题的过程的方式。 研究的第一部分将是在字符串重写系统上以最简单的形式检查该过程。 一旦开发了以最简单的形式解决单词问题的方法，这些方法将被转移回纯粹的方程逻辑中，并最终将其转移到完整的一阶方程逻辑中。 对于地面方程理论，该计划是根据研究Shostak的一致性关闭方法开发的重写范式来研究计算一致性封闭的技术。 将研究对决策程序组合的申请。 一致性封闭方法和酸形图之间的关系将进行研究和利用。 在统一中，集中度是在语义统一上，其中一些函数符号具有与之相关的语义，通常以方程式理论的形式指定。 应用程序的主要重点是自动推理和符号计算。 在过程代数中引起的电子统一问题。知识表示和约束求解器也将进行研究。 将研究理论和实际问题：（1）在理论方面，将研究各种方程统一和不分统计问题的可决定性和复杂性问题---这是过去几年所做的工作的延续； （2）在实际方面，目标是提出有效的算法以及快速实施，利用启发式方法。 实施将纳入统一算法库统一工作台中。