Termination of Ground Non-Symmetric Knuth-Bendix Completion

In the most natural approach, ground Knuth-Bendix completion procedures for non-symmetric transitive relations and quasiorderings, as specified in [16], need not terminate. We use a two-step transformation on the input expressions to enforce termination after O(n) steps in the size of the input. We apply the completion procedure for developing rule-based declarative and dynamic algorithms for detecting embeddings in ground rewrite sequences. These results are interesting for the constraint-based analysis of state transition systems, for partial evaluation and for the reachability and termination analysis of ground term rewrite systems