Improved modular termination proofs using dependency pairs

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

*Corresponding author for this work

Research output: Contribution to journalConference articleResearchpeer-review

Abstract

The dependency pair approach is one of the most powerful techniques for automated (innermost) termination proofs of term rewrite systems (TRSs). For any TRS, it generates inequality constraints that have to be satisfied by well-founded orders. However, proving innermost termination is considerably easier than termination, since the constraints for innermost termination are a subset of those for termination. We show that surprisingly, the dependency pair approach for termination can be improved by only generating the same constraints as for innermost termination. In other words, proving full termination becomes virtually as easy as proving innermost termination. Our results are based on splitting the termination proof into several modular independent subproofs. We implemented our contributions in the automated termination prover AProVE and evaluated them on large collections of examples. These experiments show that our improvements increase the power and efficiency of automated termination proving substantially.

Original languageEnglish
Book seriesLecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)
Volume3097
Pages (from-to)75-90
Number of pages16
ISSN0302-9743
Publication statusPublished - 9. Dec 2004
EventSecond International Joint Conference, IJCAR 2004 - Cork, Ireland
Duration: 4. Jul 20048. Jul 2004

Conference

ConferenceSecond International Joint Conference, IJCAR 2004
Country/TerritoryIreland
CityCork
Period04/07/200408/07/2004
SponsorScience Foundation Ireland, Cork Constraint Computation Centre, University College Cork

Fingerprint

Dive into the research topics of 'Improved modular termination proofs using dependency pairs'. Together they form a unique fingerprint.

Cite this