Termination of String Rewriting Proved Automatically

Arts, T. and Giesl, J.: Termination of term rewriting using dependency pairs, Theoret. Comput. Sci. 236 (2000), 133–178.

Ben-Cherifa, A. and Lescanne, P.: Termination of rewriting systems by polynomial interpretations and its implementation, Sci. Comput. Programming 9 (1987), 137–159.

Contejean, E., Marché, C., Monate, B. and Urbain, X.: The CiME rewrite tool, available at http://cime.lri.fr/.

Dershowitz, N.: Termination of linear rewriting systems, in S. Even and O. Kariv (eds.), Proc. of the 8th Internat. Coll. on Automata, Languages and Programming (ICALP-81), Lecture Notes in Comput. Sci. 115, Springer, Berlin, 1981, pp. 448–458.

Dershowitz, N.: Orderings for term-rewriting systems, Theoret. Comput. Sci. 17 (1982), 279–301.

Geser, A.: Relative termination, PhD Thesis, Universität Passau, Germany, 1990.

Geser, A., Hofbauer, D. and Waldmann, J.: Match-bounded string rewriting systems, in B. Rovan and P. Vojtas (eds.), Proc. of the 28th Internat. Symp. on Mathematical Foundations of Computer Science (MFCS-03), Lecture Notes in Comput. Sci. 2747, Springer, Berlin, 2003, pp. 449–459. Extended version accepted for publication in Appl. Algebra Engrg. Comm. Comput.

Geser, A., Hofbauer, D. and Waldmann, J.: Deciding termination for ancestor match-bounded string rewriting systems, Nia Technical Report, National Institute of Aerospace, Hampton, VA, 2004; available at research.nianet.org/~geser/papers/nia-ancestors.html.

Geser, A., Hofbauer, D., Waldmann, J. and Zantema, H.: Finding finite automata that certify termination of string rewriting, in K. Salomaa and S. Yu (eds.), Proc. of Ninth Internat. Conf. on Implementation and Application of Automata (CIAA04), Lecture Notes in Comput. Sci., Springer, Berlin, 2004.

Giesl, J., Thiemann, R., Schneider-Kamp, P. and Falke, S.: Automated termination proofs with AProVE, in V. van Oostrom (ed.), Proc. of the 15th Conf. on Rewriting Techniques and Applications (RTA), Lecture Notes in Comput. Sci. 3091, Springer, Berlin, 2004, pp. 210–220; tool available at http://www-i2.informatik.rwth-aachen.de/AProVE/.

Giesl, J. and Zantema, H.: Liveness in rewriting, in R. Nieuwenhuis (ed.), Proc. of the 14th Conf. on Rewriting Techniques and Applications (RTA), Lecture Notes in Comput. Sci. 2706, Springer, Berlin, 2003, pp. 321–336.

Hirokawa, N. and Middeldorp, A.: Tsukuba termination tool, in R. Nieuwenhuis (ed.), Proc. of the 14th Conf. on Rewriting Techniques and Applications (RTA), Lecture Notes in Comput. Sci. 2706, Springer, Berlin, 2003, pp. 311–320.

Hirokawa, N. and Middeldorp, A.: Dependency pairs revisited, in V. van Oostrom (ed.), Proc. of the 15th Conf. on Rewriting Techniques and Applications (RTA), Lecture Notes in Comput. Sci. 3091, Springer, Berlin, 2004, pp. 249–268.

Krishnamoorthy, M. S. and Narendran, P.: On recursive path ordering, Theoret. Comput. Sci. 40 (1985), 323–328.

Kurth, W.: Termination und Konfluenz von Semi-Thue-Systemen mit nur einer Regel, PhD Thesis, Technische Universität Clausthal, Germany, 1990.

Lagarias, J. C.: The 3n+1 problem and its generalizations, Amer. Math. Monthly 92 (1985), 3–23.

Lankford, D. S.: On proving term rewriting systems are noetherian, Technical Report MTP 3, Louisiana Technical University, 1979.

Manna, Z. and Ness, S.: On the termination of Markov algorithms, in Proc. of the Third Hawaii Internat. Conf. on System Science, Honolulu, HI, 1970, pp. 789–792.

Vardi, I.: Computational Recreations in Mathematica, Addison-Wesley, Reading, MA, 1991.

Waldmann, J.: Matchbox: A tool for match-bounded string rewriting, in V. van Oostrom (ed.), Proc. of the 15th Conf. on Rewriting Techniques and Applications (RTA), Lecture Notes in Comput. Sci. 3091, Springer, Berlin, 2004, pp. 85–94.

Zantema, H.: Termination of term rewriting: Interpretation and type elimination, J. Symbolic Comput. 17 (1994), 23–50.

Zantema, H.: Termination of term rewriting by semantic labelling, Fundamenta Informaticae 24 (1995), 89–105.

Zantema, H.: Termination, in: Term Rewriting Systems, by Terese, Cambridge Univ. Press, Cambridge, 2003, pp. 181–259.

Zantema, H.: Termination of string rewriting proved automatically, Technical Report CS-report 03-14, Eindhoven University of Technology, 2003; available via http://www.win.tue.nl/inf/onderzoek/en_index.html.

Zantema, H.: TORPA: Termination of rewriting proved automatically, in V. van Oostrom (ed.), Proc. of the 15th Conf. on Rewriting Techniques and Applications (RTA), Lecture Notes in Comput. Sci. 3091, Springer, Berlin, 2004, pp. 95–104.

Zantema, H. and Geser, A.: Non-looping string rewriting, Theoret. Informatics Appl. 33 (1999), 279–301.