A transformational approach to prove outermost termination automatically

M. Raffelsieper, H. Zantema

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

12 Citations (Scopus)
2 Downloads (Pure)

Abstract

We present transformations from a generalized form of left-linear TRSs, called quasi left-linear TRSs, to TRSs such that outermost termination of the original TRS can be concluded from termination of the transformed TRS. In this way we can apply state-of-the-art termination tools for automatically proving outermost termination of any given quasi left-linear TRS. Experiments show that this works well for non-trivial examples, some of which could not be automatically proven outermost terminating before. Therefore, our approach substantially increases the class of systems that can be shown outermost terminating automatically.
Original languageEnglish
Title of host publicationProceedings of the 8th International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2008, Castle of Hagenberg, Austria, July 14, 2008)
EditorsA. Middeldorp
Pages3-21
DOIs
Publication statusPublished - 2009

Publication series

NameElectronic Notes in Theoretical Computer Science
Volume237
ISSN (Print)1571-0061

Fingerprint Dive into the research topics of 'A transformational approach to prove outermost termination automatically'. Together they form a unique fingerprint.

Cite this