My main research interest is the unification modulo equational theories.
At the moment I am working on the development of unification algorithms for the description logics. The unification problem for the inexpressive description logic EL has been solved. Based on the algorithm for EL, we have soved unification in EL without top constructor. We have deviced a practical algorithm for another small description logic FL_0. Extension of the unification algorithms for EL to EL modulo ground axioms (GCI's) has been done to some extend... Unification in unrestricted EL modulo ground axioms is still a challenge!
Previously I was working with Chris Lynch at Clarkson University. We have designed a general algorithm for unification modulo any equational theory and several decision procedures for particular equational theories.