Improved modular termination proofs using dependency pairs

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

*Kontaktforfatter for dette arbejde

Publikation: Bidrag til tidsskriftKonferenceartikelForskningpeer review

Resumé

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.

OriginalsprogEngelsk
BogserieLecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)
Vol/bind3097
Sider (fra-til)75-90
Antal sider16
ISSN0302-9743
StatusUdgivet - 9. dec. 2004
BegivenhedSecond International Joint Conference, IJCAR 2004 - Cork, Irland
Varighed: 4. jul. 20048. jul. 2004

Konference

KonferenceSecond International Joint Conference, IJCAR 2004
LandIrland
ByCork
Periode04/07/200408/07/2004
SponsorScience Foundation Ireland, Cork Constraint Computation Centre, University College Cork

Fingeraftryk

Experiments

Citer dette

@inproceedings{c59395575ef5455fb67ae5f2fa336704,
title = "Improved modular termination proofs using dependency pairs",
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.",
author = "Ren{\'e} Thiemann and J{\"u}rgen Giesl and Peter Schneider-Kamp",
year = "2004",
month = "12",
day = "9",
language = "English",
volume = "3097",
pages = "75--90",
journal = "Lecture Notes in Computer Science",
issn = "0302-9743",
publisher = "Heinemann",

}

Improved modular termination proofs using dependency pairs. / Thiemann, René; Giesl, Jürgen; Schneider-Kamp, Peter.

I: Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science), Bind 3097, 09.12.2004, s. 75-90.

Publikation: Bidrag til tidsskriftKonferenceartikelForskningpeer review

TY - GEN

T1 - Improved modular termination proofs using dependency pairs

AU - Thiemann, René

AU - Giesl, Jürgen

AU - Schneider-Kamp, Peter

PY - 2004/12/9

Y1 - 2004/12/9

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=9444229424&partnerID=8YFLogxK

M3 - Conference article

VL - 3097

SP - 75

EP - 90

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

SN - 0302-9743

ER -