Mechanizing and improving dependency pairs

Jürgen Giesl*, René Thiemann, Peter Schneider-Kamp, Stephan Falke

*Kontaktforfatter for dette arbejde

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review


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.

TidsskriftJournal of Automated Reasoning
Udgave nummer3
Sider (fra-til)155-203
Antal sider49
StatusUdgivet - 1. okt. 2006