Jürgen Giesl, René Thiemann, Peter Schneider-Kamp, and Stephan Falke:
Mechanizing and Improving Dependency Pairs
Journal of Automated Reasoning 37(3), pages 155-203, 2006. ©Springer-Verlag
The dependency pair technique 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 that simplify (innermost) termination proofs
significantly. 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.
[
BibTeX
|
Preliminary Version (ps.gz)
|
Preliminary Version (pdf)
|
Paper on SpringerLink
]