Paper Description: MIP-9608

BibTeX entry:

@incollection{MIP-9608,
author="A. Geser",
title="Omega-Termination is Undecidable for Totally Terminating Term Rewriting Systems",
institution="Fakult{\"a}t f{\"u}r Mathematik und Informatik, Universit{\"a}t Passau",
year=1996,
number={MIP-9608}
}

Abstract:

We give a complete proof of the fact that the following problem is undecidable:
Given: A term rewriting system, where the termination of its rewrite relation is provable by a total reduction order on ground terms,
Wanted: Does there exist a strictly monotonic interpretation in the positive integers that proves termination?
Keywords: term rewriting, termination, total termination, omega-termination, termination hierarchy, termination type

Paper itself:

Cross links:

Ulrike Peiker, Martin Griebl