An Introduction to Knuth-Bendix Completion
A. J. J. Dick · The Computer Journal · 1991
An informal introduction is given to the underlying concepts of term rewriting. Topics covered and Knuth-Bendix completion, completion modulo equations, unfailing completion and theorem proving by completion