books.google.co.uk - This textbook offers a unified, self-contained introduction to the field of term rewriting. Baader and Nipkow cover all the basic material--abstract reduction systems, termination, confluence, completion, and combination problems--but also some important and closely connected subjects: universal algebra,...http://books.google.co.uk/books/about/Term_Rewriting_and_All_That.html?id=N7BvXVUCQk8C&q=holds&utm_source=gb-gplus-shareTerm Rewriting and All That
