Equality Reasoning: Word and Unification Problems

这个项目涉及方程推理，重点是单词和统一问题。研究包括图、同余闭包和等式统一，以及这些主题的进一步发展，以及这些主题的组合。目标是开发新的可判定性和复杂性结果，并设计和实现有效的算法。解决文字问题的方法将使用重写范式，集中于计算完整/规范的重写规则集的过程和数据结构。特别地，我们将研究使用SOUR图来完成重写系统的方法，特别是如何使用SOUR图来开发解决某些类别理论中的单词问题的程序。研究的第一部分将以其最简单的形式，对字符串重写系统进行检查。一旦开发出以最简单形式解决单词问题的方法，这些方法将被移回纯方程逻辑，并最终进入全一阶方程逻辑。对于基础方程理论，计划是研究基于在研究肖斯塔克的同余闭包方法中开发的重写范式计算同余闭包的技术。对决策程序组合的应用将进行调查。研究了同余闭包方法与SOUR图之间的关系。在统一中，重点是语义统一，其中一些函数符号具有与之相关的语义，通常以方程理论的形式指定。应用程序的主要焦点是自动推理和符号计算。过程代数中的e -统一问题。知识表示和约束求解器也将被研究。将研究理论和实践问题：(1)在理论方面，将研究各种方程统一和不统一问题的可决性和复杂性问题——这是过去几年所做工作的延续；(2)在实践方面，目标是利用启发式，提出高效的算法和快速的实现。实现将被合并到统一工作台中，这是一个统一算法库。

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.