Automating the Knuth Bendix Ordering

Knuth and Bendix proposed a very versatile technique for ordering terms, based upon assigning weights to operators and then to terms by adding up the weights of the operators they contain. Our purpose in this paper is as follows. First we give some examples to indicate the flexibility of the method. Then we give a simple and practical algorithm, based on solving systems of linear inequalities, for determining whether or not a set of rules can be ordered by a Knuth Bendix ordering. We also describe how this algorithm may be incorporated in a completion procedure which thus considers all possible choices of weights which orient a given equation.