A Characterization of Quasi-Decreasingness

Thomas Sternagel and Christian Sternagel

Proceedings of the 15th International Workshop on Termination (WST 2016), pp. 12:1 – 12:5, 2016.


In 2010 Schernhammer and Gramlich showed that quasi-decreasingness of a DCTRS R is equivalent to µ-termination of its context-sensitive unraveling Ucs® on original terms. While the direction that quasi-decreasingness of R implies µ-termination of Ucs® on original terms is shown directly; the converse – facilitating the use of context-sensitive termination tools like MU-TERM and VMTL – employs the additional notion of context-sensitive quasi-reductivity of R. In the following, we give a direct proof of the fact that µ-termination of Ucs® on original terms implies quasi-decreasingness of R. Moreover, we report our experimental findings on DCTRSs from the confluence problems database (Cops), extending the experiments of Schernhammer and Gramlich.




author = "Thomas Sternagel and Christian Sternagel",
title = "A Characterization of Quasi-Decreasingness",
booktitle = "Proceedings of the 5th International Workshop on Termination",
pages = "12:1--12:5",
year = 2016
Nach oben scrollen