Equality Reasoning: Word and Unification Problems

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

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 various eq uational 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.