Abstract

For a hierarchy of properties of term rewriting systems related to termination we prove relative undecidability: For implications X ⇒ Y in the hierarchy the property X is undecidable for term rewriting systems satisfying Y. For most implications we obtain this result for term rewriting systems consisting of a single rewrite rule.

BibTeX Entry

@article{GMOZ-IC02a,
 author    = "Alfons Geser and Aart Middeldorp and Enno Ohlebusch and Hans
              Zantema",
 title     = "Relative Undecidability in the Term Rewriting, Part 1: The
              Termination Hierarchy",
 journal   = "Information and Computation",
 volume    = 178,
 number    = 1,
 pages     = "101--131",
 year      = 2002,
 doi       = "10.1006/inco.2002.3120"
}