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.

  • 1
    $\begingroup$ Have you tried to look at the 581 articles citing this one? scholar.google.com/scholar?cites=3988217028093045034 $\endgroup$ May 28, 2013 at 6:29
  • $\begingroup$ I have, but I can't say I found what I need. It is hard for me as a newbie to distill relevant papers from such a big pile. I thought maybe there is someone who works on this and who can provide some overview. $\endgroup$
    – bellpeace
    May 29, 2013 at 0:13

1 Answer 1


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)


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.