Abstract

The match-bound technique is a recent and elegant method to prove the
termination of rewrite systems using automata techniques. To increase the
applicability of the method we incorporate it into the dependency
pair framework. The key to this is the introduction of two new enrichments
which take the special properties of dependency pair problems into
account.

BibTeX

@inproceedings{MKAM-LATA08,
  author      = "Martin Korp and Aart Middeldorp",
  title       = "Match-Bounds with Dependency Pairs for Proving Termination
                 of Rewrite Systems",
  booktitle   = "Proceedings of the 2nd International Conference on
                 Language and Automata Theory and Applications",
  series      = "Lecture Notes in Computer Science",
  publisher   = "Springer-Verlag",
  volume      = 5196,
  year        = 2008,
  pages       = "321--332"
}