Transforming Dependency Chains of Constrained TRSs into Bounded Monotone Sequences of Integers

Tomohiro Sasano, Naoki Nishida, Masahiko Sakai +1

In the dependency pair framework for proving termination of rewriting systems, polynomial interpretations are used to transform dependency chains into bounded decreasing sequences…