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.
The two obvious references are:

Chapter 7 of Term Rewriting and All That, notable for its pedagogy and accessible examples

Chapter 7 of Term Rewriting Systems, notable for its completeness and attention to detail, though a bit dated at this point I guess.


Note that neither refers to completion as &quot;Knuth-Bendix&quot; 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?