Proving Termination by Dependency Pairs and Inductive Theorem Proving
Identifieur interne : 002355 ( Istex/Curation ); précédent : 002354; suivant : 002356Proving Termination by Dependency Pairs and Inductive Theorem Proving
Auteurs : Carsten Fuhs [Allemagne] ; Jürgen Giesl [Allemagne] ; Michael Parting [Allemagne] ; Peter Schneider-Kamp [Danemark] ; Stephan Swiderski [Allemagne]Source :
- Journal of Automated Reasoning [ 0168-7433 ] ; 2011-08-01.
English descriptors
- KwdEn :
Abstract
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.
Url:
DOI: 10.1007/s10817-010-9215-9
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: Pour aller vers cette notice dans l'étape Curation :002386
Links to Exploration step
ISTEX:99B5DE0CD006C840C4A13B7F45A198B745D6DADFLe document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Proving Termination by Dependency Pairs and Inductive Theorem Proving</title><author><name sortKey="Fuhs, Carsten" sort="Fuhs, Carsten" uniqKey="Fuhs C" first="Carsten" last="Fuhs">Carsten Fuhs</name><affiliation wicri:level="1"><mods:affiliation>LuFG Informatik 2, RWTH Aachen University, Aachen, Germany</mods:affiliation><country xml:lang="fr">Allemagne</country><wicri:regionArea>LuFG Informatik 2, RWTH Aachen University, Aachen</wicri:regionArea></affiliation></author><author><name sortKey="Giesl, Jurgen" sort="Giesl, Jurgen" uniqKey="Giesl J" first="Jürgen" last="Giesl">Jürgen Giesl</name><affiliation wicri:level="1"><mods:affiliation>LuFG Informatik 2, RWTH Aachen University, Aachen, Germany</mods:affiliation><country xml:lang="fr">Allemagne</country><wicri:regionArea>LuFG Informatik 2, RWTH Aachen University, Aachen</wicri:regionArea></affiliation><affiliation wicri:level="1"><mods:affiliation>E-mail: giesl@informatik.rwth-aachen.de</mods:affiliation><country wicri:rule="url">Allemagne</country></affiliation></author><author><name sortKey="Parting, Michael" sort="Parting, Michael" uniqKey="Parting M" first="Michael" last="Parting">Michael Parting</name><affiliation wicri:level="1"><mods:affiliation>LuFG Informatik 2, RWTH Aachen University, Aachen, Germany</mods:affiliation><country xml:lang="fr">Allemagne</country><wicri:regionArea>LuFG Informatik 2, RWTH Aachen University, Aachen</wicri:regionArea></affiliation></author><author><name sortKey="Schneider Kamp, Peter" sort="Schneider Kamp, Peter" uniqKey="Schneider Kamp P" first="Peter" last="Schneider-Kamp">Peter Schneider-Kamp</name><affiliation wicri:level="1"><mods:affiliation>Department of Mathematics & Computer Science, University of Southern Denmark, Odense, Denmark</mods:affiliation><country xml:lang="fr">Danemark</country><wicri:regionArea>Department of Mathematics & Computer Science, University of Southern Denmark, Odense</wicri:regionArea></affiliation></author><author><name sortKey="Swiderski, Stephan" sort="Swiderski, Stephan" uniqKey="Swiderski S" first="Stephan" last="Swiderski">Stephan Swiderski</name><affiliation wicri:level="1"><mods:affiliation>LuFG Informatik 2, RWTH Aachen University, Aachen, Germany</mods:affiliation><country xml:lang="fr">Allemagne</country><wicri:regionArea>LuFG Informatik 2, RWTH Aachen University, Aachen</wicri:regionArea></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:99B5DE0CD006C840C4A13B7F45A198B745D6DADF</idno><date when="2011" year="2011">2011</date><idno type="doi">10.1007/s10817-010-9215-9</idno><idno type="url">https://api.istex.fr/ark:/67375/VQC-6STSK0F7-5/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">002386</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002386</idno><idno type="wicri:Area/Istex/Curation">002355</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Proving Termination by Dependency Pairs and Inductive Theorem Proving</title><author><name sortKey="Fuhs, Carsten" sort="Fuhs, Carsten" uniqKey="Fuhs C" first="Carsten" last="Fuhs">Carsten Fuhs</name><affiliation wicri:level="1"><mods:affiliation>LuFG Informatik 2, RWTH Aachen University, Aachen, Germany</mods:affiliation><country xml:lang="fr">Allemagne</country><wicri:regionArea>LuFG Informatik 2, RWTH Aachen University, Aachen</wicri:regionArea></affiliation></author><author><name sortKey="Giesl, Jurgen" sort="Giesl, Jurgen" uniqKey="Giesl J" first="Jürgen" last="Giesl">Jürgen Giesl</name><affiliation wicri:level="1"><mods:affiliation>LuFG Informatik 2, RWTH Aachen University, Aachen, Germany</mods:affiliation><country xml:lang="fr">Allemagne</country><wicri:regionArea>LuFG Informatik 2, RWTH Aachen University, Aachen</wicri:regionArea></affiliation><affiliation wicri:level="1"><mods:affiliation>E-mail: giesl@informatik.rwth-aachen.de</mods:affiliation><country wicri:rule="url">Allemagne</country></affiliation></author><author><name sortKey="Parting, Michael" sort="Parting, Michael" uniqKey="Parting M" first="Michael" last="Parting">Michael Parting</name><affiliation wicri:level="1"><mods:affiliation>LuFG Informatik 2, RWTH Aachen University, Aachen, Germany</mods:affiliation><country xml:lang="fr">Allemagne</country><wicri:regionArea>LuFG Informatik 2, RWTH Aachen University, Aachen</wicri:regionArea></affiliation></author><author><name sortKey="Schneider Kamp, Peter" sort="Schneider Kamp, Peter" uniqKey="Schneider Kamp P" first="Peter" last="Schneider-Kamp">Peter Schneider-Kamp</name><affiliation wicri:level="1"><mods:affiliation>Department of Mathematics & Computer Science, University of Southern Denmark, Odense, Denmark</mods:affiliation><country xml:lang="fr">Danemark</country><wicri:regionArea>Department of Mathematics & Computer Science, University of Southern Denmark, Odense</wicri:regionArea></affiliation></author><author><name sortKey="Swiderski, Stephan" sort="Swiderski, Stephan" uniqKey="Swiderski S" first="Stephan" last="Swiderski">Stephan Swiderski</name><affiliation wicri:level="1"><mods:affiliation>LuFG Informatik 2, RWTH Aachen University, Aachen, Germany</mods:affiliation><country xml:lang="fr">Allemagne</country><wicri:regionArea>LuFG Informatik 2, RWTH Aachen University, Aachen</wicri:regionArea></affiliation></author></analytic><monogr></monogr><series><title level="j">Journal of Automated Reasoning</title><title level="j" type="abbrev">J Autom Reasoning</title><idno type="ISSN">0168-7433</idno><idno type="eISSN">1573-0670</idno><imprint><publisher>Springer Netherlands</publisher><pubPlace>Dordrecht</pubPlace><date type="published" when="2011-08-01">2011-08-01</date><biblScope unit="volume">47</biblScope><biblScope unit="issue">2</biblScope><biblScope unit="page" from="133">133</biblScope><biblScope unit="page" to="160">160</biblScope></imprint><idno type="ISSN">0168-7433</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0168-7433</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Dependency pairs</term><term>Induction</term><term>Term rewriting</term><term>Termination</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">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.</div></front></TEI></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002355 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Curation/biblio.hfd -nk 002355 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Curation
|type= RBID
|clé= ISTEX:99B5DE0CD006C840C4A13B7F45A198B745D6DADF
|texte= Proving Termination by Dependency Pairs and Inductive Theorem Proving
}}
| This area was generated with Dilib version V0.6.33. |  |