In: Nipkow, T.: Lecture Notes in Computer Science, Vol. 1379: 9th International Conf. RTA'98 Rewriting Techniques and Applications, Tsukuba, Japan, pages 166-180. April 1998.
Abstract: In this paper we initiate a study of polynomial-time reductions for some basic decision problems of rewrite systems. We the give a pollynomial-time algorithm for Unique-normal-form property of ground systems for the first time. Next we prove undecidability of these problems for a fixed string rewriting system using our reductions. Finally, we prove partial decidability results for Confluence of Commutative semi-thue systems. The Confluence and Unique-normal-form property are shown Expspace-hard of commutative semi-thue systems. We also show that there is a family of string rewrite systems for which the world problem is trivially decidable but confluence undecidable, and we show a linear equational theory with decidable word problem but undecidable linear equational matching.