License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.05431.6
URN: urn:nbn:de:0030-drops-5091
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2006/509/
Go to the corresponding Portal

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

Proving and Disproving Termination in the Dependency Pair Framework

pdf-format:
05431.GieslJuergen.ExtAbstract.509.pdf (0.07 MB)

Abstract

The dependency pair framework is a new general concept to integrate
arbitrary techniques for termination analysis of term rewriting.
In this way, the benefits of different techniques can be combined and
their modularity and power are increased significantly. Moreover, this
framework facilitates the development of new methods for termination analysis.

Traditionally, the research on termination focused on methods which
prove termination and there were hardly any approaches for disproving
termination. We show that with the dependency pair framework, one
can combine the search for a proof and for a disproof of termination.
In this way, we obtain the first powerful method which can also
verify non-termination of term rewrite systems.

We implemented and evaluated our contributions in the automated termination
prover AProVE. Due to these results, AProVE was the winning tool in the
International Competition of Termination Provers 2005, both for proving and
for disproving termination of term rewriting.

BibTeX - Entry

@InProceedings{giesl_et_al:DagSemProc.05431.6,
  author =	{Giesl, J\"{u}rgen and Thiemann, Ren\'{e} and Schneider-Kamp, Peter},
  title =	{{Proving and Disproving Termination in the Dependency Pair Framework}},
  booktitle =	{Deduction and Applications},
  pages =	{1--1},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5431},
  editor =	{Franz Baader and Peter Baumgartner and Robert Nieuwenhuis and Andrei Voronkov},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2006/509},
  URN =		{urn:nbn:de:0030-drops-5091},
  doi =		{10.4230/DagSemProc.05431.6},
  annote =	{Keywords: Termination, non-termination, term rewriting, dependency pairs}
}

Keywords: Termination, non-termination, term rewriting, dependency pairs
Collection: 05431 - Deduction and Applications
Issue Date: 2006
Date of publication: 25.04.2006

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI