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

@inproceedings{MKAM-CADE09,
  author    = "Martin Korp and Aart Middeldorp",
  title     = "Beyond Dependency Graphs",
  booktitle = "Proceedings of the 22nd International Conference on
               Automated Deduction",
  address   = "Montreal",
  series    = "Lecture Notes in Artificial Intelligence",
  volume    = 5663,
  pages     = "339--354",
  year      = 2009
}