Automating the Knuth Bendix Ordering

Ursula Hilda Mary Martin, AJJ Dick, JR Kalmus

Research output: Contribution to journalArticlepeer-review

30 Citations (Scopus)


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
Publication statusPublished - 1990




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

Cite this