Equality Reasoning: Word and 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.