Knuth–Bendix completion

Summary

Knuth–Bendix completion is a procedure that turns a set of equations into a term rewriting system. The rules of the result are oriented by a well-founded order, and the system is confluent. It orients the equations into rules, looks for critical pairs where two rules overlap, and adds new rules until all overlaps resolve. When it succeeds, every term has a unique normal form, and equality modulo the equations is decided by comparing normal forms. It may also fail or run forever, as it must, since the word problem for groups is undecidable in general.