The following technical report is available from
http://aib.informatik.rwth-aachen.de/:
Jürgen Giesl, René Thiemann,
Peter Schneider-Kamp, Stephan Falke
Mechanizing Dependency Pairs
2003-08
Abstract:
The dependency pair approach is a powerful technique
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 approach 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.
