A Transformational Approach to Prove Outermost Termination Automatically
Matthias Raffelsieper, Hans Zantema · Electronic Notes in Theoretical Computer Science · 2009
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.