M. Alpuente, M. Comini, S. Escobar, M. Falaschi, and S. Lucas, Abstract diagnosis of functional programs, Proc. of the 12th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR'02), vol.2664, pp.1-16, 2003.

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.

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.

M. Alpuente, M. Falaschi, G. Moreno, and G. Vidal, Rules + strategies for transforming lazy functional logic programs, Theoretical Computer Science, vol.311, issue.1-3, pp.479-525, 2004.

M. Alpuente, M. Falaschi, M. Ramis, and G. Vidal, Narrowing approximations as an optimization for equational logic programs, Proc. of the 5th International Symposium on Programming Language Implementation and Logic Programming (PLILP'93), vol.714, pp.391-409, 1993.

, AProVE's 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.

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.

J. Chabin and P. Réty, Narrowing directed by a graph of terms, Proc. of the 4th International Conference on Rewriting Techniques and Applications (RTA'91), vol.488, pp.112-123, 1991.

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

P. Cousot and R. Cousot, Abstract interpretation: a unifed lattice model for static analysis of programs by construction or approximation of fixpoints, Proc. of the 4th Symposium on Principles of Programming Languages (POPL'77), pp.238-252, 1977.

P. Cousot and N. Halbwachs, Automatic discovery of linear restraints among variables of a program, Proc. of the 5th Symposium on Principles of Programming Languages (POPL'78), pp.84-96, 1978.

N. Dershowitz, Termination of linear rewriting systems, Proc. of the 8th International Colloquium on Automata, Languages and Programming (ICALP'81), vol.115, pp.448-458, 1981.

N. Dershowitz, Termination of rewriting, Journal of Symbolic Computation, vol.3, issue.1 & 2, pp.69-116, 1987.

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

N. Eén and N. Sörensson, An extensible SAT-solver, Proc. of the 6th International Conference on Theory and Applications of Satisfiability Testing (SAT'03), vol.2919, pp.502-518, 2004.

M. Gabbrielli and R. Giacobazzi, Goal independency and call patterns in the analysis of logic programs, Proc. of the ACM Symposium on Applied Computing (SAC'94), pp.394-399, 1994.

S. Genaim and M. Codish, Inferring termination condition for logic programs using backwards analysis, Artificial intelligence and Reasoning (LPAR'01), vol.2250, pp.685-694, 2001.

A. Geser, D. Hofbauer, and J. Waldmann, Deciding termination for ancestor match-bounded string rewriting systems, 2004.

A. Geser and H. Zantema, Non-looping string rewriting, RAIRO Theoretical Informatics and Applications, vol.33, pp.279-301, 1999.

J. Giesl, P. Schneider-kamp, and R. Thiemann, AProVE 1.2: Automatic termination proofs in the dependency pair framework, Proc. of the 3rd International Joint Conference on Automated Reasoning (IJCAR'06), vol.4130, pp.281-286, 2006.

J. Giesl, R. Thiemann, and P. Schneider-kamp, The dependency pair framework: combining techniques for automated termination proofs, Proc. of the 11th International Conference on Logic for Programming, Artificial intelligence and Reasoning (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 the 5th International Workshop on Frontiers of Combining Systems (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 the 15th International Conference on Rewriting Techniques and Applications (RTA'04), vol.3091, pp.210-220, 2004.

J. V. Guttag, D. Kapur, and D. R. Musser, On proving uniform termination and restricted termination of rewriting systems, SIAM Journal of Computing, vol.12, issue.1, pp.189-214, 1983.

M. Hanus, The integration of functions into logic programming: From theory to practice, Journal of Logic Programming, vol.19, pp.583-628, 1994.

N. Hirokawa and A. Middeldorp, Tyrolean Termination Tool: Techniques and features, Information and Computation, vol.205, issue.4, pp.474-511, 2007.

S. Hölldobler, Foundations of Equational Logic Programming, Lecture Notes in Artificial Intelligence, vol.353, 1989.

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

W. Kurth, Termination und konfluenz von semi-Thue-systemen mit nur einer regel, 1990.

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

C. Marché and H. Zantema, The termination competition, Proc. of Term Rewriting and Applications, 18th International Conference (RTA'07), vol.4533, pp.303-313, 2007.

, Matchbox's web site

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

E. Payet, Detecting non-termination of term rewriting systems using an unfolding operator, Proc. of the 16th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR'06), vol.4407, pp.194-209, 2007.
URL : https://hal.archives-ouvertes.fr/hal-01916159

E. Payet and F. Mesnard, Non-termination inference for constraint logic programs, Proc. of the 11th International Symposium on Static Analysis (SAS'04), vol.3148, pp.377-392, 2004.

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 Computing Surveys, vol.28, issue.2, pp.360-414, 1996.

D. A. Schmidt, A calculus of logical relations for over-and underapproximating static analyses, Science of Computer Programming, vol.64, issue.1, pp.29-53, 2007.

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

A. Tarski, A lattice theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics, vol.5, pp.285-310, 1955.

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.

, TTT2's web site

J. Waldmann, Matchbox: A tool for match-bounded string rewriting, Proc. of the 15th International Conference on Rewriting Techniques and Applications (RTA'04), vol.3091, pp.85-94, 2004.

J. Waldmann, Compressed loops (draft), 2007.

H. Zankl and A. Middeldorp, Nontermination of string rewriting using SAT, Proc. of the 9th International Workshop on Termination (WST'07), pp.52-55, 2007.

H. Zantema, Termination of string rewriting proved automatically, Journal of Automated Reasoning, vol.34, issue.2, pp.105-139, 2005.