Mechanizing and Improving Dependency Pairs

9 years 9 months ago
Mechanizing and Improving Dependency Pairs
The dependency pair technique [1, 11, 12] is a powerful method for automated termination and innermost termination proofs of term rewrite systems (TRSs). For any TRS, it generates inequality constraints that have to be satisfied by well-founded orders. We improve the dependency pair technique by considerably reducing the number of constraints produced for (innermost) termination proofs. Moreover, we extend transformation techniques to manipulate dependency pairs which simplify (innermost) termination proofs significantly. In order to fully mechanize the approach, we show how transformations and the search for suitable orders can be mechanized efficiently. We implemented our results in the automated termination prover AProVE and evaluated them on large collections of examples.
Jürgen Giesl, René Thiemann, Peter Sch
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2006
Where JAR
Authors Jürgen Giesl, René Thiemann, Peter Schneider-Kamp, Stephan Falke
Comments (0)