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.

• Type: Journal
• Year: 2006
• Where: JAR
• Authors: Jürgen Giesl, René Thiemann, Peter Schneider-Kamp, Stephan Falke
• Keywords: Dependency Pair Technique, Innermost Termination Proofs, JAR 2006, Termination Proofs