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.

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