Improving context-sensitive dependency Pairs

Beatriz Alarcón*, Fabian Emmes, Carsten Fuhs, Jürgen Giesl, Raúl Gutiérrez, Salvador Lucas, Peter Schneider-Kamp, René Thiemann

*Kontaktforfatter for dette arbejde

Publikation: Bidrag til bog/antologi/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer review

Resumé

Context-sensitive dependency pairs (CS-DPs) are currently the most powerful method for automated termination analysis of context-sensitive rewriting. However, compared to DPs for ordinary rewriting, CS-DPs suffer from two main drawbacks: (a) CS-DPs can be collapsing. This complicates the handling of CS-DPs and makes them less powerful in practice. (b) There does not exist a "DP framework" for CS-DPs which would allow one to apply them in a flexible and modular way. This paper solves drawback (a) by introducing a new definition of CS-DPs. With our definition, CS-DPs are always non-collapsing and thus, they can be handled like ordinary DPs. This allows us to solve drawback (b) as well, i.e., we extend the existing DP framework for ordinary DPs to context-sensitive rewriting. We implemented our results in the tool AProVE and successfully evaluated them on a large collection of examples.

OriginalsprogEngelsk
TitelLogic for Programming, Artificial Intelligence, and Reasoning - 15th International Conference, LPAR 2008, Proceedings
Antal sider16
Publikationsdato31. dec. 2008
Sider636-651
ISBN (Trykt)3540894381, 9783540894384
DOI
StatusUdgivet - 31. dec. 2008
Begivenhed15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2008 - Doha, Qatar
Varighed: 22. nov. 200827. nov. 2008

Konference

Konference15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2008
LandQatar
ByDoha
Periode22/11/200827/11/2008
SponsorQatar National Research Fund, Qatar Science and Technology Park (QSTP), iHorizons, Carnegie Mellon University, Microsoft Research, Kurt Godel Society
NavnLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Vol/bind5330 LNAI
ISSN0302-9743

Citer dette

Alarcón, B., Emmes, F., Fuhs, C., Giesl, J., Gutiérrez, R., Lucas, S., ... Thiemann, R. (2008). Improving context-sensitive dependency Pairs. I Logic for Programming, Artificial Intelligence, and Reasoning - 15th International Conference, LPAR 2008, Proceedings (s. 636-651). Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind. 5330 LNAI https://doi.org/10.1007/978-3-540-89439-1_44
Alarcón, Beatriz ; Emmes, Fabian ; Fuhs, Carsten ; Giesl, Jürgen ; Gutiérrez, Raúl ; Lucas, Salvador ; Schneider-Kamp, Peter ; Thiemann, René. / Improving context-sensitive dependency Pairs. Logic for Programming, Artificial Intelligence, and Reasoning - 15th International Conference, LPAR 2008, Proceedings. 2008. s. 636-651 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 5330 LNAI).
@inproceedings{da57b55c0ed04da6bfc12724e1d93b84,
title = "Improving context-sensitive dependency Pairs",
abstract = "Context-sensitive dependency pairs (CS-DPs) are currently the most powerful method for automated termination analysis of context-sensitive rewriting. However, compared to DPs for ordinary rewriting, CS-DPs suffer from two main drawbacks: (a) CS-DPs can be collapsing. This complicates the handling of CS-DPs and makes them less powerful in practice. (b) There does not exist a {"}DP framework{"} for CS-DPs which would allow one to apply them in a flexible and modular way. This paper solves drawback (a) by introducing a new definition of CS-DPs. With our definition, CS-DPs are always non-collapsing and thus, they can be handled like ordinary DPs. This allows us to solve drawback (b) as well, i.e., we extend the existing DP framework for ordinary DPs to context-sensitive rewriting. We implemented our results in the tool AProVE and successfully evaluated them on a large collection of examples.",
author = "Beatriz Alarc{\'o}n and Fabian Emmes and Carsten Fuhs and J{\"u}rgen Giesl and Ra{\'u}l Guti{\'e}rrez and Salvador Lucas and Peter Schneider-Kamp and Ren{\'e} Thiemann",
year = "2008",
month = "12",
day = "31",
doi = "10.1007/978-3-540-89439-1_44",
language = "English",
isbn = "3540894381",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Heinemann",
pages = "636--651",
booktitle = "Logic for Programming, Artificial Intelligence, and Reasoning - 15th International Conference, LPAR 2008, Proceedings",

}

Alarcón, B, Emmes, F, Fuhs, C, Giesl, J, Gutiérrez, R, Lucas, S, Schneider-Kamp, P & Thiemann, R 2008, Improving context-sensitive dependency Pairs. i Logic for Programming, Artificial Intelligence, and Reasoning - 15th International Conference, LPAR 2008, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), bind 5330 LNAI, s. 636-651, 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2008, Doha, Qatar, 22/11/2008. https://doi.org/10.1007/978-3-540-89439-1_44

Improving context-sensitive dependency Pairs. / Alarcón, Beatriz; Emmes, Fabian; Fuhs, Carsten; Giesl, Jürgen; Gutiérrez, Raúl; Lucas, Salvador; Schneider-Kamp, Peter; Thiemann, René.

Logic for Programming, Artificial Intelligence, and Reasoning - 15th International Conference, LPAR 2008, Proceedings. 2008. s. 636-651 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 5330 LNAI).

Publikation: Bidrag til bog/antologi/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer review

TY - GEN

T1 - Improving context-sensitive dependency Pairs

AU - Alarcón, Beatriz

AU - Emmes, Fabian

AU - Fuhs, Carsten

AU - Giesl, Jürgen

AU - Gutiérrez, Raúl

AU - Lucas, Salvador

AU - Schneider-Kamp, Peter

AU - Thiemann, René

PY - 2008/12/31

Y1 - 2008/12/31

N2 - Context-sensitive dependency pairs (CS-DPs) are currently the most powerful method for automated termination analysis of context-sensitive rewriting. However, compared to DPs for ordinary rewriting, CS-DPs suffer from two main drawbacks: (a) CS-DPs can be collapsing. This complicates the handling of CS-DPs and makes them less powerful in practice. (b) There does not exist a "DP framework" for CS-DPs which would allow one to apply them in a flexible and modular way. This paper solves drawback (a) by introducing a new definition of CS-DPs. With our definition, CS-DPs are always non-collapsing and thus, they can be handled like ordinary DPs. This allows us to solve drawback (b) as well, i.e., we extend the existing DP framework for ordinary DPs to context-sensitive rewriting. We implemented our results in the tool AProVE and successfully evaluated them on a large collection of examples.

AB - Context-sensitive dependency pairs (CS-DPs) are currently the most powerful method for automated termination analysis of context-sensitive rewriting. However, compared to DPs for ordinary rewriting, CS-DPs suffer from two main drawbacks: (a) CS-DPs can be collapsing. This complicates the handling of CS-DPs and makes them less powerful in practice. (b) There does not exist a "DP framework" for CS-DPs which would allow one to apply them in a flexible and modular way. This paper solves drawback (a) by introducing a new definition of CS-DPs. With our definition, CS-DPs are always non-collapsing and thus, they can be handled like ordinary DPs. This allows us to solve drawback (b) as well, i.e., we extend the existing DP framework for ordinary DPs to context-sensitive rewriting. We implemented our results in the tool AProVE and successfully evaluated them on a large collection of examples.

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

U2 - 10.1007/978-3-540-89439-1_44

DO - 10.1007/978-3-540-89439-1_44

M3 - Article in proceedings

AN - SCOPUS:58049125849

SN - 3540894381

SN - 9783540894384

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 636

EP - 651

BT - Logic for Programming, Artificial Intelligence, and Reasoning - 15th International Conference, LPAR 2008, Proceedings

ER -

Alarcón B, Emmes F, Fuhs C, Giesl J, Gutiérrez R, Lucas S et al. Improving context-sensitive dependency Pairs. I Logic for Programming, Artificial Intelligence, and Reasoning - 15th International Conference, LPAR 2008, Proceedings. 2008. s. 636-651. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 5330 LNAI). https://doi.org/10.1007/978-3-540-89439-1_44