Automating the Knuth Bendix ordering

Jeremy Dick, John Kalmus, Ursula Martin

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

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.
Original languageEnglish
Pages (from-to)95-119
Number of pages25
JournalActa Informatica
Issue number2
Publication statusPublished - 1 Feb 1990


Dive into the research topics of 'Automating the Knuth Bendix ordering'. Together they form a unique fingerprint.

Cite this