M. Alpuente, M. Falaschi, and F. Manzo, Analyses of unsatisfiability for equational logic programming, Journal of Logic Programming, vol.311, issue.1-3, pp.479-525, 1995.
DOI : 10.1016/0743-1066(94)00024-z
URL : https://doi.org/10.1016/0743-1066(94)00024-z

M. Alpuente, M. Falaschi, G. Moreno, and G. Vidal, Safe folding/unfolding with conditional narrowing, Proc. of ALP/HOA 97, pp.1-15, 1997.
DOI : 10.1007/bfb0026999

M. Alpuente, M. Falaschi, G. Moreno, and G. Vidal, Rules + strategies for transforming lazy functional logic programs, Theoretical Computer Science, vol.311, issue.13, pp.479-525, 2004.
DOI : 10.1016/j.tcs.2003.10.033
URL : https://doi.org/10.1016/j.tcs.2003.10.033

M. Alpuente, M. Falaschi, M. J. Ramis, and G. Vidal, Narrowing approximations as an optimization for equational logic programs, Proc. of PLILP 1993, pp.391-409, 1993.
DOI : 10.1007/3-540-57186-8_93

T. Arts and J. Giesl, Termination of term rewriting using dependency pairs. Theoretical Computer Science, vol.236, pp.133-178, 2000.
DOI : 10.1016/s0304-3975(99)00207-8
URL : https://doi.org/10.1016/s0304-3975(99)00207-8

F. Baader and T. Nipkow, Term rewriting and all that, 1998.

R. M. Burstall and J. Darlington, A transformation system for developing recursive programs, Journal of the ACM, vol.24, issue.1, pp.44-67, 1977.
DOI : 10.1145/321992.321996

J. Chabin and P. Réty, Narrowing directed by a graph of terms, Proc. of RTA'91, vol.488, pp.112-123, 1991.

M. Codish and C. Taboch, A semantic basis for the termination analysis of logic programs, Journal of Logic Programming, vol.41, issue.1, pp.103-123, 1999.

N. Dershowitz, Termination of rewriting, Journal of Symbolic Computation, vol.3, issue.1 & 2, pp.69-116, 1987.
DOI : 10.1016/s0747-7171(87)80022-6
URL : https://doi.org/10.1016/s0747-7171(87)80022-6

K. Drosten, Termersetzungssysteme: Grundlagen der Prototyp-Generierung algebraischer Spezifikationen, 1989.

M. Gabbrielli and R. Giacobazzi, Goal independency and call patterns in the analysis of logic programs, Proc. of SAC'94, pp.394-399, 1994.

S. Genaim and M. Codish, Inferring termination conditions for logic programs using backwards analysis, Proc. of LPAR'01, vol.2250, pp.685-694, 2001.

J. Giesl, R. Thiemann, and P. Schneider-kamp, The dependency pair framework: combining techniques for automated termination proofs, Proc. of LPAR'04, vol.3452, pp.210-220, 2004.

J. Giesl, R. Thiemann, and P. Schneider-kamp, Proving and disproving termination of higher-order functions, Proc. of FroCoS'05, vol.3717, pp.216-231, 2005.

J. Giesl, R. Thiemann, P. Schneider-kamp, and S. Falke, Automated termination proofs with AProVE, Proc. of RTA'04, vol.3091, pp.210-220, 2004.
DOI : 10.1007/978-3-540-25979-4_15
URL : http://www-i2.informatik.rwth-aachen.de/giesl/papers/RTA04-distribute.pdf

D. Kapur, D. Musser, P. Narendran, and J. Stillman, Semi-unification, Theoretical Computer Science, vol.81, pp.169-187, 1991.
DOI : 10.1007/3-540-50517-2_95

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

F. Mesnard and R. Bagnara, cTI: a constraint-based termination inference tool for iso-prolog, Theory and Practice of Logic Programming, vol.5, issue.1-2, pp.243-257, 2005.

E. Payet and F. Mesnard, Non-termination inference for constraint logic programs, Proc. of SAS'04, vol.3148, pp.377-392, 2004.
DOI : 10.1007/978-3-540-27864-1_27

E. Payet and F. Mesnard, Non-termination inference of logic programs, ACM Transactions on Programming Languages and Systems, vol.28, pp.256-289, 2006.
URL : https://hal.archives-ouvertes.fr/hal-00129526

A. Pettorossi and M. Proietti, Rules and strategies for transforming functional and logic programs, ACM Comput. Surv, vol.28, issue.2, pp.360-414, 1996.

J. Steinbach, Simplification orderings: history of results, Fundamenta Informaticae, vol.24, pp.47-87, 1995.

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.