Sciweavers

RTA
1997
Springer

Proving Innermost Normalisation Automatically

14 years 2 months ago
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.
Thomas Arts, Jürgen Giesl
Added 08 Aug 2010
Updated 08 Aug 2010
Type Conference
Year 1997
Where RTA
Authors Thomas Arts, Jürgen Giesl
Comments (0)