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 "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?
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”.