tr-announce February 2007

tr-announce@lists.rwth-aachen.de

1 participants
2 discussions

2007-03: Proving Termination by Bounded Increase

by Peter Schneider-Kamp

The following technical report is available from http://aib.informatik.rwth-aachen.de: Proving Termination by Bounded Increase Jürgen Giesl, René Thiemann, Stephan Swiderski, and Peter Schneider-Kamp AIB 2007-03 Most methods and tools for termination analysis of term rewrite systems (TRSs) essentially try to find arguments of functions that decrease in recursive calls. However, they fail if the reason for termination is that an argument is increased in recursive calls repeatedly until it reaches a bound. In this paper, we solve that problem and present a method to prove termination of TRSs with bounded increase automatically.

17 years, 7 months

2007-02: SAT Solving for Termination Analysis with Polynomial Interpretations

by Peter Schneider-Kamp

The following technical report is available from http://aib.informatik.rwth-aachen.de: SAT Solving for Termination Analysis with Polynomial Interpretations Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, René Thiemann, and Harald Zankl AIB 2007-02 Polynomial interpretations are one of the most popular techniques for automated termination analysis. Therefore, the search for such interpretations is a main bottleneck in most termination provers. We show that one can obtain speedups in orders of magnitude by encoding this task as a SAT problem and by applying modern SAT solvers.

17 years, 8 months

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

2001

tr-announce February 2007