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.