Knuth-Bendix Completion for Non-Symmetric Transitive Relations
Georg Struth · Electronic Notes in Theoretical Computer Science · 2001
We extend the Knuth-Bendix completion procedure from equational rewriting to rewriting with non-symmetric transitive relations and quasi-orderings. The main differences are the following: Specification of the general non-ground case seems beyond first-order logic. It is within that realm when terms are linear or functions non-monotonic. The procedure requires critical-pair computations and need not terminate even in the ground case. Simplification is not don't care non-deterministic, but search based. Applications include ordered resolution and ordered chaining calculi, development of rule-based declarative procedures and algorithms, program and reachability analysis (in rewriting logic) and propagation of inequality constraints.