Mechanizing and Improving Dependency Pairs
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. The authors improve the dependency pair technique by considerably reducing the number of constraints produced for (innermost) termination proofs. Moreover, they extend transformation techniques to manipulate dependency pairs which simplify (innermost) termination proofs significantly. In order to fully mechanize the approach, they show how transformations and the search for suitable orders can be mechanized efficiently.