Termination by quasi-periodic interpretations

H. Zantema, J. Waldmann

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

3 Citations (Scopus)
85 Downloads (Pure)


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.
Original languageEnglish
Title of host publicationProceedings of the 18th International Conference on Term Rewriting and Applications (RTA 2007) 26-28 June 2007, Paris, France
EditorsF. Baader
ISBN (Print)978-3-540-73447-5
Publication statusPublished - 2007
Eventconference; RTA 2007, Paris, France; 2007-06-26; 2007-06-28 -
Duration: 26 Jun 200728 Jun 2007

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Conferenceconference; RTA 2007, Paris, France; 2007-06-26; 2007-06-28
OtherRTA 2007, Paris, France

Cite this