Abstract
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. © Springer-Verlag Berlin Heidelberg 2007.
Cite
CITATION STYLE
Ludwig, M., & Waldmann, U. (2007). An extension of the Knuth-Bendix ordering with LPO-like properties. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4790 LNAI, pp. 348–362). Springer Verlag. https://doi.org/10.1007/978-3-540-75560-9_26
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
