Proving Innermost Normalisation Automatically

We present a technique to prove innermost normalisation of term rewriting systems TRSs automatically. In contrast to previous methods, our technique is able to prove innermost normalisation of TRSs that are not terminating. Our technique can also be used for termination proofs of all TRSs where innermost normalisation implies termination, such as non-overlapping TRSs or locally con uent overlay systems. In this way, termination of many also non-simply terminating TRSs can be veri ed automatically.

• Type: Conference
• Year: 1997
• Where: RTA
• Authors: Thomas Arts, Jürgen Giesl
• Keywords: Innermost Normalisation, Normalisation Implies Termination, RTA 1997, Term Rewriting Systems, Theoretical Computer Science