Abstract

The dependency pair framework is a powerful technique for proving termination of rewrite systems. One of the most frequently used methods within this framework is the dependency graph processor. In this paper we improve this processor by incorporating right-hand sides of forward closures. In combination with tree automata completion we obtain an efficient processor which can be used instead of the dependency graph approximations that are in common use in termination provers.

BibTeX Entry

@inproceedings{KM-CADE09,
 author    = "Martin Korp and Aart Middeldorp",
 title     = "Beyond Dependency Graphs",
 booktitle = "Proceedings of the 22nd International Conference on Automated
              Deduction",
 series    = "Lecture Notes in Artificial Intelligence",
 volume    = 5663,
 pages     = "339--354",
 year      = 2009,
 doi       = "10.1007/978-3-642-02959-2\_26"
}