Proving Termination by Dependency Pairs and Inductive Theorem Proving

Carsten Fuhs, Jürgen Giesl, Peter Schneider-Kamp, Michael Parting

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

Resumé

Current techniques and tools for automated termination analysis of term rewrite systems (TRSs) are already very powerful. However, they fail for algorithms whose termination is essentially due to an inductive argument. Therefore, we show how to couple the dependency pair method for termination of TRSs with inductive theorem proving. As confirmed by the implementation of our new approach in the tool AProVE, now TRS termination techniques are also successful on this important class of algorithms.
OriginalsprogEngelsk
TidsskriftJournal of Automated Reasoning
Vol/bind47
Udgave nummer2
Sider (fra-til)133-160
ISSN0168-7433
DOI
StatusUdgivet - 2011

Fingeraftryk

Theorem proving

Citer dette

Fuhs, Carsten ; Giesl, Jürgen ; Schneider-Kamp, Peter ; Parting, Michael. / Proving Termination by Dependency Pairs and Inductive Theorem Proving. I: Journal of Automated Reasoning. 2011 ; Bind 47, Nr. 2. s. 133-160.
@article{b8d16143a15a4d6193473b7e6494d8f6,
title = "Proving Termination by Dependency Pairs and Inductive Theorem Proving",
abstract = "Current techniques and tools for automated termination analysis of term rewrite systems (TRSs) are already very powerful. However, they fail for algorithms whose termination is essentially due to an inductive argument. Therefore, we show how to couple the dependency pair method for termination of TRSs with inductive theorem proving. As confirmed by the implementation of our new approach in the tool AProVE, now TRS termination techniques are also successful on this important class of algorithms.",
author = "Carsten Fuhs and J{\"u}rgen Giesl and Peter Schneider-Kamp and Michael Parting",
year = "2011",
doi = "10.1007/s10817-010-9215-9",
language = "English",
volume = "47",
pages = "133--160",
journal = "Journal of Automated Reasoning",
issn = "0168-7433",
publisher = "Springer",
number = "2",

}

Proving Termination by Dependency Pairs and Inductive Theorem Proving. / Fuhs, Carsten; Giesl, Jürgen; Schneider-Kamp, Peter; Parting, Michael.

I: Journal of Automated Reasoning, Bind 47, Nr. 2, 2011, s. 133-160.

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

TY - JOUR

T1 - Proving Termination by Dependency Pairs and Inductive Theorem Proving

AU - Fuhs, Carsten

AU - Giesl, Jürgen

AU - Schneider-Kamp, Peter

AU - Parting, Michael

PY - 2011

Y1 - 2011

N2 - Current techniques and tools for automated termination analysis of term rewrite systems (TRSs) are already very powerful. However, they fail for algorithms whose termination is essentially due to an inductive argument. Therefore, we show how to couple the dependency pair method for termination of TRSs with inductive theorem proving. As confirmed by the implementation of our new approach in the tool AProVE, now TRS termination techniques are also successful on this important class of algorithms.

AB - Current techniques and tools for automated termination analysis of term rewrite systems (TRSs) are already very powerful. However, they fail for algorithms whose termination is essentially due to an inductive argument. Therefore, we show how to couple the dependency pair method for termination of TRSs with inductive theorem proving. As confirmed by the implementation of our new approach in the tool AProVE, now TRS termination techniques are also successful on this important class of algorithms.

U2 - 10.1007/s10817-010-9215-9

DO - 10.1007/s10817-010-9215-9

M3 - Journal article

VL - 47

SP - 133

EP - 160

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

IS - 2

ER -