Abstract

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.

BibTeX Entry

@inproceedings{KM-RTA07,
 author    = "Martin Korp and Aart Middeldorp",
 title     = "Proving Termination of Rewrite Systems using Bounds",
 booktitle = "Proceedings of the 18th International Conference on Rewriting
              Techniques and Applications",
 series    = "Lecture Notes in Computer Science",
 volume    = 4533,
 pages     = "273--287",
 year      = 2007,
 doi       = "10.1007/978-3-540-73449-9\_21"
}