Mechanizing and improving dependency pairs

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

*Kontaktforfatter for dette arbejde

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

Resumé

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.

OriginalsprogEngelsk
TidsskriftJournal of Automated Reasoning
Vol/bind37
Udgave nummer3
Sider (fra-til)155-203
Antal sider49
ISSN0168-7433
DOI
StatusUdgivet - 1. okt. 2006

Citer dette

Giesl, Jürgen ; Thiemann, René ; Schneider-Kamp, Peter ; Falke, Stephan. / Mechanizing and improving dependency pairs. I: Journal of Automated Reasoning. 2006 ; Bind 37, Nr. 3. s. 155-203.
@article{d38178ec567a41c1908b02471e00c8d1,
title = "Mechanizing and improving dependency pairs",
abstract = "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.",
keywords = "Dependency pairs, Term rewriting, Termination",
author = "J{\"u}rgen Giesl and Ren{\'e} Thiemann and Peter Schneider-Kamp and Stephan Falke",
year = "2006",
month = "10",
day = "1",
doi = "10.1007/s10817-006-9057-7",
language = "English",
volume = "37",
pages = "155--203",
journal = "Journal of Automated Reasoning",
issn = "0168-7433",
publisher = "Springer",
number = "3",

}

Mechanizing and improving dependency pairs. / Giesl, Jürgen; Thiemann, René; Schneider-Kamp, Peter; Falke, Stephan.

I: Journal of Automated Reasoning, Bind 37, Nr. 3, 01.10.2006, s. 155-203.

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

TY - JOUR

T1 - Mechanizing and improving dependency pairs

AU - Giesl, Jürgen

AU - Thiemann, René

AU - Schneider-Kamp, Peter

AU - Falke, Stephan

PY - 2006/10/1

Y1 - 2006/10/1

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

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

KW - Dependency pairs

KW - Term rewriting

KW - Termination

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

U2 - 10.1007/s10817-006-9057-7

DO - 10.1007/s10817-006-9057-7

M3 - Journal article

AN - SCOPUS:33846578613

VL - 37

SP - 155

EP - 203

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

IS - 3

ER -