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.