Knuth and Bendix ordering (KBO) is an algorithm for ordering terms based on assigning non-negative integer weights to operators and then to terms by adding up the weights of the operators they contain. Terms are compared by lexicographically comparing first the weights, then the outermost operators, and then the subterms. KBO is easy to implement, fast to execute, and flexible, but it has some problems. The most serious problem is that it is difficult to know what weights to choose.

This paper provides a simple and practical procedure, based on solving systems of linear inequalities, for determining whether a set of rules can be ordered by KBO. At each stage are a set of rules and a system of inequalities that has a solution, proving termination of the rules. When a new rule is to be considered, the system of inequalities is extended appropriately. If the extended system has a solution, then a KBO exists for the set of rules that includes the new rule.