> I think Edsko was more specifically referring to the book "Term > Rewriting and all That" by Baader and Nipkow. Thanks for pointing this out--I was confused. I notice the book has a chapter on equational unification that includes a section on AC unification. This book looks like a winner. Thank you. John