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

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