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 Entry

@article{KM-IC09,
 author    = "Martin Korp and Aart Middeldorp",
 title     = "Match-Bounds Revisited",
 journal   = "Information and Computation",
 volume    = 207,
 number    = 11,
 pages     = "1259-1283",
 year      = 2009,
 doi       = "10.1016/j.ic.2009.02.010"
}