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.
|Title of host publication||Proceedings of the 8th International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2008, Castle of Hagenberg, Austria, July 14, 2008)|
|Publication status||Published - 2009|
|Name||Electronic Notes in Theoretical Computer Science|