Proving Termination of Constrained Term Rewriting Systems


In this presentation, I propose methods for proving termination of
constrained term rewriting systems, where constraints are interpreted by
built-in semantics given by users, and rewrite rules are sound for the
interpretation, i.e., the interpretation of term is preserved under the
reduction. The method for proving termination is a straightforward
extension of the dependency pair framework for unconstrained term rewriting
systems.