[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #22 (Solved !)

Originator: Nachum Dershowitz
Date: April 1991

Summary: Devise practical methods for proving termination of conditional rewriting systems.

Devise practical methods for proving termination of (standard) conditional rewriting systems. Part of the difficulty stems from the interdependence of normalization and termination.


Termination and decreasingness of CTRSs can be proved by transforming CTRSs into unconditional TRSs such that termination of the TRS is sufficient for decreasingness of the CTRS. Several variants of this transformation are studied in [BK86, DP86, GA01, GM87, Siv89, Mar96, Ohl01]. Termination of the TRSs resulting from this transformation can often be proved automatically using dependency pairs [AG00, GA01]. The transformation (together with the dependency pair approach) is implemented in the tools TALP [OCM00] and AProVE [GTSKF04]. Both tools use this transformation in order to show termination of logic programs, but AProVE can also prove termination and decreasingness of CTRSs in this way. A different approach for termination proofs of CTRSs with the general path order [DH95] is described in [Hoo96].


Thomas Arts and Jürgen Giesl. Termination of term rewriting using dependency pairs. Theoretical Computer Science, 236:133–178, 2000.
J. A. Bergstra and Jan Willem Klop. Conditional rewrite rules: Confluency and termination. Journal of Computer and System Sciences, 32(3):323–362, 1986.
Nachum Dershowitz and Charles Hoot. Natural termination. Theoretical Computer Science, 142:170–207, 1995.
Nachum Dershowitz and David Plaisted. Equational programming. Machine Intelligence, 11:21–56, 1986.
Jürgen Giesl and Thomas Arts. Verification of Erlang processes by dependency pairs. Applicable Algebra in Engineering, Communication and Computing, 12(1,2):39–72, 2001.
E. Giovanetti and C. Moiso. Notes on the elimination of conditions. In Proc. CTRS ’87, LNCS 308, pages 91–97, 1987.
Jürgen Giesl, René Thiemann, Peter Schneider-Kamp, and S. Falke. Automated termination proofs with AProVE. In Vincent van Oostrom, editor, 15th International Conference on Rewriting Techniques, volume 3091 of Lecture Notes in Computer Science, pages 210–220, Aachen, Germany, June 2004. Springer-Verlag.
Charles Hoot. Termination of Non-Simple Rewrite Systems. PhD thesis, University of Illinois, 1996.
M. Marchiori. Unravelings and ultra-properties. In Proc. ALP ’96, LNCS 1139, pages 107–121, 1996.
Enno Ohlebusch, Claus Claves, and Claude Marché. TALP: A tool for the termination analysis of logic programs. In Leo Bachmair, editor, Rewriting Techniques and Applications, volume 1833 of Lecture Notes in Computer Science, pages 270–273, Norwich, UK, July 2000. Springer-Verlag.
Enno Ohlebusch. Termination of logic programs: Transformational methods revisited. Applicable Algebra in Engineering, Communication and Computing, 12(1,2):73–116, 2001.
G. Sivakumar. Proofs and Computations in Conditional Equational Theories. PhD thesis, Department of Computer Science, University of Illinois, Urbana, IL, May 1989. Report R-89-1642.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]