We present a new method for automatically proving termination of term rewriting and string rewriting. It is based on the well-known idea of interpretation of terms in natural numbers where every rewrite step causes a decrease. In the dependency pair setting only weak monotonicity is required for these interpretations. For these we use quasi-periodic functions. It turns out that then the decreasingness for rules only needs to be checked for finitely many values, which is easy to implement.
Using this technique we automatically prove termination of over ten string rewriting systems in TPDB for which termination was open until now.
|Name||Lecture Notes in Computer Science|
|Conference||conference; RTA 2007, Paris, France; 2007-06-26; 2007-06-28|
|Period||26/06/07 → 28/06/07|
|Other||RTA 2007, Paris, France|