Abstract

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.

BibTeX

@inproceedings{TSCS-WST16,
 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
}