Beyond Dependency Graphs

Martin Korp and Aart Middeldorp

Proceedings of the 22nd International Conference on Automated Deduction (CADE 2009), Lecture Notes in Artificial Intelligence 5663, pp. 339 – 354, 2009.


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.


  PDF |    doi:10.1007/978-3-642-02959-2_26  |  © Springer


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
Nach oben scrollen