Total Termination of Term Rewriting

Usually termination of term rewriting systems TRS's is proved by means of a monotonic well-founded order. If this order is total on ground terms, the TRS is called totally terminating. In this paper we prove that total termination is an undecidable property of nite term rewriting systems. The proof is given by means of Post's Correspondence Problem.

• Type: Conference
• Year: 1993
• Where: RTA
• Authors: Maria C. F. Ferreira, Hans Zantema
• Keywords: Monotonic Well-founded Order, RTA 1993, Term Rewriting Systems, Theoretical Computer Science, Total Termination