Automating the Knuth Bendix ordering
Automating the Knuth Bendix ordering
复制标题
自动化 Knuth Bendix 订购
作者：
J. Dick;J. Kalmus;U. Martin
Knuth和Benidol提出了一种非常通用的术语排序技术，该技术基于将权重分配给运算符，然后通过将它们包含的运算符的权重相加来分配给术语。本文的目的如下。首先，我们给出了一些例子来说明该方法的灵活性。然后，我们给出了一个简单而实用的算法，解决线性不等式组的基础上，确定是否一组规则可以排序的Knuth Beneficiary顺序。我们还描述了如何将该算法可以被纳入一个完整的过程，从而考虑所有可能的选择的权重定向一个给定的方程。
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.