State-of-the-art unification for associative-commutative functions I am interested what are the open problems on unification methods for associative-commutative functions, and what is the state-of-the-art work? I have found some old work, but nothing new. I am wondering if I am missing something since I am quite new to this.

It might help to say that I am generally interested in this area as I would like to apply it to modern programming languages, in terms of code canonicalization.
Here are the standard references on unification:


Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, United Kingdom, 1998. (Book homepage)
Franz Baader and Wayne Snyder. Unification Theory. In J.A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, pages 447-533. Elsevier Science Publishers, 2001. (Online copy here)