Proving Termination of Rewrite Systems Using Bounds

The use of automata techniques to prove the termination of string rewrite systems and left-linear term rewrite systems is advocated by Geser et al. in a recent sequence of papers. We extend their work to non-left-linear rewrite systems. The key to this extension is the introduction of so-called raise rules and the use of tree automata that are not quite deterministic. Furthermore, we present negative solutions to two open problems related to string rewrite systems.

• Type: Conference
• Year: 2007
• Where: RTA
• Authors: Martin Korp, Aart Middeldorp
• Keywords: Left-linear Term Rewrite, Rewrite Systems, RTA 2007, String Rewrite Systems, Theoretical Computer Science