Termination of rewriting is undecidable in the one-rvle case

1. R.V. Book, Thue Systems as Rewriting Systems, in: J.P. Jouannaud, ed., Proceedings of the First International Conference on Rewriting Techniques and Applications, Dijon, France. Springer Lec. Notes Comp. Sci.202 (1985) 63–94. Revised version: J. Symbolic Computation, 3 (1987) 39–68.

   Google Scholar 

2. N. Dershowitz, Termination, in: J.P. Jouannaud, ed., Proceedings of the First International Conference on Rewriting Techniques and Applications, Dijon, France. Springer Lec. Notes Comp. Sci.202 (1985) 180–224. Revised version: Termination of rewiting. J. Symbolic Computation, 3 (1987) 69–116.

   Google Scholar 

3. J.V. Guttag, D. Kapur and D.R. Musser, On proving uniform termination and restricted termination of rewriting systems. SIAM J. Comput.12 (1983) 187–214.

   Google Scholar 

4. G. Huet, D.S. Lankfork, On the uniform halting problem for term rewriting systems, Rapport Laboria 283 (1978), INRIA, Le Chesnay, France.

   Google Scholar 

5. G. Huet and D.C. Oppen, Equations and rewrite rules: A survey, in: R.V. Book, ed., Formal Language Theory: Perspectives and Open Problems, 1980, pp. 349–405. New York: Academic Press.

   Google Scholar 

6. J.P. Jouannaud, Editorial of J. Symbolic Computation, 3, 1–2, 1987, 1–2.

   Google Scholar 

7. R. Lipton and L. Snyder, On the halting of tree replacement systems. Proceedings of the Conference on Theoretical Computer Science, University of Waterloo, Waterloo, Canada, (1977), 43–46.

   Google Scholar 

Download references