Sciweavers

58
Voted
LPAR
2004
Springer

The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs

14 years 5 months ago
The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs
The dependency pair approach is one of the most powerful techniques for automated termination proofs of term rewrite systems. Up to now, it was regarded as one of several possible methods to prove termination. In this paper, we show that dependency pairs can instead be used as a general concept to integrate arbitrary techniques for termination analysis. In this way, the benefits of different techniques can be combined and their modularity and power are increased significantly. We refer to this new concept as the “dependency pair framework” to distinguish it from the old “dependency pair approach”. Moreover, this framework facilitates the development of new methods for termination analysis. To demonstrate this, we present several new techniques within the dependency pair framework which simplify termination problems considerably. We implemented the dependency pair framework in our termination prover AProVE and evaluated it on large collections of examples.
Jürgen Giesl, René Thiemann, Peter Sch
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where LPAR
Authors Jürgen Giesl, René Thiemann, Peter Schneider-Kamp
Comments (0)