M. Alpuente, M. Falaschi, G. Moreno, and G. Vidal, Safe folding/unfolding with conditional narrowing, Proc. of Algebraic and Logic Programming, 6th International Joint Conference (ALP/HOA 97, vol.1298, pp.1-15, 1997.
DOI : 10.1007/bfb0026999
URL : http://www.dsic.upv.es/users/elp/german/alp97/paper.pdf

, AProVE Web site

T. Arts and J. Giesl, Termination of term rewriting using dependency pairs. Theoretical Computer Science, vol.236, pp.133-178, 2000.

F. Baader and T. Nipkow, Term Rewriting and All That, 1998.

J. Giesl, C. Aschermann, M. Brockschmidt, F. Emmes, F. Frohn et al., Analyzing program termination and complexity automatically with AProVE, Journal of Automated Reasoning, vol.58, issue.1, pp.3-31, 2017.

D. Kapur, D. Musser, P. Narendran, and J. Stillman, Semi-unification, Theoretical Computer Science, vol.81, issue.2, pp.169-187, 1991.

D. S. Lankford and D. R. Musser, A finite termination criterion. Unpublished Draft, USC Information Sciences Institute, 1978.

´. E. Payet, Loop detection in term rewriting using the eliminating unfoldings. Theoretical Computer Science, vol.403, pp.307-327, 2008.
URL : https://hal.archives-ouvertes.fr/hal-01186183

, Termination Portal-An (incomplete) overview of existing tools for termination analysis

, Termination Problems Data Base

Y. Toyama, Counterexamples to the termination for the direct sum of term rewriting systems, Information Processing Letters, vol.25, issue.3, pp.141-143, 1987.