caa a22 4500 467989699 CHVBK 20180323112541.0 cr unu---uuuuu 170328e19900201xx s 000 0 eng 10.1007/BF01237233 doi (NATIONALLICENCE)springer-10.1007/BF01237233 Automating the Knuth Bendix ordering [Elektronische Daten] [Jeremy Dick, John Kalmus, Ursula Martin] 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. Springer-Verlag, 1990 Dick Jeremy Informatics Department, Rutherford Appleton Laboratory, Chilton, OX11 0QX, Didcot, Oxon, UK aut Kalmus John Informatics Department, Rutherford Appleton Laboratory, Chilton, OX11 0QX, Didcot, Oxon, UK aut Martin Ursula Department of Computer Science, Royal Holloway and Bedford New College, University of London, Egham Hill, TW20 0EX, Egham, Surrey, UK aut Acta Informatica Springer-Verlag 28/2(1990-02-01), 95-119 0001-5903 28:2<95 1990 28 236 https://doi.org/10.1007/BF01237233 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/BF01237233 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Dick Jeremy Informatics Department, Rutherford Appleton Laboratory, Chilton, OX11 0QX, Didcot, Oxon, UK aut NATIONALLICENCE 700 1- Kalmus John Informatics Department, Rutherford Appleton Laboratory, Chilton, OX11 0QX, Didcot, Oxon, UK aut NATIONALLICENCE 700 1- Martin Ursula Department of Computer Science, Royal Holloway and Bedford New College, University of London, Egham Hill, TW20 0EX, Egham, Surrey, UK aut NATIONALLICENCE 773 0- Acta Informatica Springer-Verlag 28/2(1990-02-01), 95-119 0001-5903 28:2<95 1990 28 236 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer