A clear and rigorous explanation of critical pairs and the Knuth-Bendix completion algorithm?

I'm looking for an explanation of critical pairs and the Knuth-Bendix completion algorithm that is at once rigorous and of high pedagogical value, i.e. clear, detailed, containing illustrative examples preferably with drawings, and reasonably self-contained. It can be inside a book, an article, lecture notes, website, whatever. Possible languages: English, French, German.

• You should find that in any textbook on term rewriting. – Jan Johannsen Oct 27 '20 at 13:23
• @JanJohannsen: That is obvious. The question was not "where can I find an explanation of critical pairs", but "where can I find a clear and rigorous explanation of critical pairs". Answering this question requires judgement and personal familiarity with specific textbooks or other sources. Not all sources are equally good answers to this question. – Evan Aad Oct 27 '20 at 13:42

The two obvious references are:

Note that neither refers to completion as "Knuth-Bendix" completion in the index, since the science of completion has come a long way since it was first introduced. This survey by Dershowitz and Jouannaud might be a bit more historical.

It might help to understand what your needs are, since the field is vast, and somewhat technical. Are you trying to use a completion algorithm? Implement it? Adapt it to a specific setting?

• "It might help to understand what your needs are" -- My goal is to understand what critical pairs are, what the Knuth-Bendix algorithm is, why it is correct, what purpose the concept of "critical pairs" serves and what purpose the algorithm serves. I became familiar with this algorithm by reading Sperschneider & Antoniou's "Logic: A Foundation for Computer Science" (Addison-Wesley, 1991), but I don't like the explanation given there and I'm looking for an alternative. – Evan Aad Oct 30 '20 at 15:58
• Critical pairs are a reasonably simple concept, heck, the wikipedia page is not too bad: en.wikipedia.org/wiki/Critical_pair_(logic). Completion algorithms are more complex, and the papers I gave give a reasonable first stab. – cody Oct 30 '20 at 21:58

There is a rather technically-detailed description to be found in any of the following:

D.F. Holt, D.B.A. Epstein, and S. Rees. The use of knuth-bendix methods to solve the word problem in automatic groups. J. Symbolic Computation, 12:397--414, 1991.

Charles C. Sims. Computation with Finitely Presented Groups. Cambridge, 1994.

Derek F. Holt. The warwick automatic groups software. In Proceedings of DIMACS Conference on Computational Group Theory, Rutgers, March 1994

A more informal, easily readable description can be found in Geoff Smith’s “Topics in Group Theory”.