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 Entry

@inproceedings{KM-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",
 volume    = 5196,
 pages     = "321--332",
 year      = 2008,
 doi       = "10.1007/978-3-540-88282-4\_30"
}