<p>Here are the standard references on unification:</p>

<ul>
<li><p>Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, United Kingdom, 1998. (<a href="http://www4.in.tum.de/~nipkow/TRaAT/" rel="nofollow">Book homepage</a>)</p></li>
<li><p>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. (<a href="http://lat.inf.tu-dresden.de/research/papers/2001/BaaderSnyderHandbook.ps.gz" rel="nofollow">Online copy here</a>)</p></li>
</ul>

CC BY-SA 3.0
2013-05-30T10:06:35.803Z
2013-05-30T10:06:35.803Z
Neel Krishnaswami
<p>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 <a href="http://dl.acm.org/citation.cfm?id=322262" rel="nofollow">some</a> <a href="http://link.springer.com/chapter/10.1007/3-540-10009-1_25" rel="nofollow">old</a> <a href="http://link.springer.com/chapter/10.1007/3-540-10009-1_25" rel="nofollow">work</a>, but nothing new. I am wondering if I am missing something since I am quite new to this.</p>

<p>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. </p>

CC BY-SA 3.0
2013-05-28T06:29:14.470Z
Have you tried to look at the 581 articles citing this one?  http://scholar.google.com/scholar?cites=3988217028093045034
András Salamon
CC BY-SA 3.0
2013-05-29T00:13:34.150Z
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.
zpavlinovic
<pl.programming-languages><term-rewriting-systems>
State-of-the-art unification for associative-commutative functions
zpavlinovic
# State-of-the-art unification for associative-commutative functions

(Asked by: username_0 on 2013-05-28)

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](http://dl.acm.org/citation.cfm?id=322262) [old](http://link.springer.com/chapter/10.1007/3-540-10009-1_25) [work](http://link.springer.com/chapter/10.1007/3-540-10009-1_25), 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.

**Tags:** pl.programming-languages, term-rewriting-systems

> **Comments:**
> **username_1**: Have you tried to look at the 581 articles citing this one?  http://scholar.google.com/scholar?cites=3988217028093045034  
> **username_0**: 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.  

---

## 1 answers

### Answer by username_2 on 2013-05-30. Score: 3 | Accepted answer

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](http://www4.in.tum.de/~nipkow/TRaAT/))
* 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](http://lat.inf.tu-dresden.de/research/papers/2001/BaaderSnyderHandbook.ps.gz))


---

