An introduction to Knuth-Bendix completion
An introduction to Knuth-Bendix completion / J.W. Klop, A. Middeldorp