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

@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",
  publisher   = "Springer-Verlag",
  year        = 2007,
  volume      = 4533,
  pages       = "273--287"
}