Research on Unification and Related Problems

这个项目研究统一，重点是语义统一，其中一些功能符号与它们相关，通常以方程理论的形式指定。主要目标是探索可判定性和复杂性结果，并在约束范式的框架内设计有效的算法，约束范式是在研究结合-交换理论的最优统一算法时开发的一种方法。特别是，正在探索使用约束和基于约束的启发式来精简搜索空间。各种方程不统一问题的可决性和复杂性问题也正在被探讨。

This project investigates unification with a focus on semantic unification where some of the function symbols have associated with them, usually specified in the form of an equational theory. The main objective is to explore decidability and complexity results, and design efficient algorithms in the framework of the constraint paradigm, an approach developed earlier in the study of optimal unification algorithms for associative-commutative theories. In particular, the use of constraints and heuristics based on them is being explored to prune the search space. Decidability and complexity issues on various equational disunification problems are also being explored.