An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
An Extension of the Knuth-Bendix Ordering with LPO-Like Properties
复制标题
具有类似 LPO 性质的 Knuth-Bendix 排序的扩展
DOI：
10.1007/978-3-540-75560-9_26
复制
发表时间：
2007
影响因子：
5
通讯作者：
Uwe Waldmann
中科院分区：
文献类型：
--
作者：
Michel Ludwig;Uwe Waldmann
在分解和叠加的成功实现中，Knuth-Bendex排序通常优于字典序路径排序，但它不符合层次叠加演算的某些要求。此外，它不允许以自然的方式定向非线性定义方程。我们提出了Knuth-Bendex排序的一个扩展，它使得克服这些限制成为可能。
The Knuth-Bendix ordering is usually preferred over the lexicographic path ordering in successful implementations of resolution and superposition, but it is incompatible with certain requirements of hierarchic superposition calculi. Moreover, it does not allow non-linear definition equations to be oriented in a natural way. We present an extension of the Knuth-Bendix ordering that makes it possible to overcome these restrictions.