Term Orderings for Non-reachability of (Conditional) Rewriting
Akihisa Yamada · Lecture notes in computer science · 2022
Abstract We propose generalizations of reduction pairs, well-established techniques for proving termination of term rewriting, in order to prove unsatisfiability of reachability (infeasibility) in plain and conditional term rewriting. We adapt the weighted path order, a merger of the Knuth–Bendix order and the lexicographic path order, into the proposed framework. The proposed approach is implemented in the termination prover , and the strength of our approach is demonstrated through examples and experiments.