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, to increase the applicability of
the method we show how it can be incorporated into the dependency pair
framework. To achieve this we introduce two new enrichments which take
the special properties of dependency pair problems into account.

BibTeX

@article{MKAM-IC09,
  author      = "Martin Korp and Aart Middeldorp",
  title       = "Match-Bounds Revisited",
  journal     = "Information and Computation",
  volume      = 207,
  number      = 11,
  pages       = "1259--1283",
  year        = 2009
}