T. Arts and J. Giesl, Proving innermost normalisation automatically, Proceedings 8th Conference on Rewriting Techniques and Applications, Sitges (Spain), pp.157-171, 1997.
DOI : 10.1007/3-540-62950-5_68

P. Borovansk´yborovansk´y, C. Kirchner, P. Héì-ene-kirchner, C. Moreau, and . Ringeissen, An overview of ELAN, Proceedings of the second International Workshop on Rewriting Logic and Applications Electronic Notes in Theoretical Computer Science, 1998.

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-oliet et al., Maude: specification and programming in rewriting logic, Theoretical Computer Science, vol.285, issue.2, pp.187-243, 2002.
DOI : 10.1016/S0304-3975(01)00359-0

H. Comon, Disunification: a survey, Computational Logic. Essays in honor of Alan Robinson, chapter 9, pp.322-359, 1991.

N. Dershowitz, Orderings for term-rewriting systems, Theoretical Computer Science, vol.17, issue.3, pp.279-301, 1982.
DOI : 10.1016/0304-3975(82)90026-3

N. Dershowitz and J. Jouannaud, Handbook of Theoretical Computer Science, volume B, chapter 6: Rewrite Systems, pp.244-320, 1990.

O. Fissore, I. Gnaedig, and H. Kirchner, Termination of rewriting with local strategies, Selected papers of the 4th International Workshop on Strategies in Automated Deduction, 2001.

O. Fissore, I. Gnaedig, and H. Kirchner, CARIBOO : An induction based proof tool for termination with strategies, Proceedings of the Fourth International Conference on Principles and Practice of Declarative Programming, pp.62-73, 2002.
URL : https://hal.archives-ouvertes.fr/inria-00107557

O. Fissore, I. Gnaedig, and H. Kirchner, Outermost Ground Termination, Proceedings of the Fourth International Workshop on Rewriting Logic and Its Applications, 2002.
DOI : 10.1016/S1571-0661(05)82535-6
URL : https://hal.archives-ouvertes.fr/inria-00099654

K. Futatsugi and A. Nakagawa, An overview of CAFE specification environment-an algebraic approach for creating, verifying, and maintaining formal specifications over networks, Proceedings First IEEE International Conference on Formal Engineering Methods, 1997.
DOI : 10.1109/ICFEM.1997.630424

I. Gnaedig, H. Kirchner, and O. Fissore, Induction for innermost and outermost ground termination, 2001.
URL : https://hal.archives-ouvertes.fr/inria-00100696

. Goubault-larreck, Well-Founded Recursive Relations, Proc. 15th Int. Workshop Computer Science Logic (CSL'2001), 2001.
DOI : 10.1007/3-540-44802-0_34

J. Goubault-larrecq, A proof of weak termination of typed lambda-sigma-calculi, Proceedings of the TYPES'96 Workshop, 1998.

B. Gramlich, Relating innermost, weak, uniform and modular termination of term rewriting systems, Proceedings of the 3rd International Conference on Logic Programming and Automated Reasoning (LPAR'92), pp.285-296, 1992.
DOI : 10.1007/BFb0013069

B. Gramlich, On termination and confluence properties of disjoint and constructor-sharing conditional rewrite systems, Theoretical Computer Science, vol.165, issue.1, pp.97-131, 1996.
DOI : 10.1016/0304-3975(96)00042-4

G. Huet and J. Lévy, Computations in orthogonal rewriting systems, I, Computational Logic, pp.395-414, 1991.

P. Klint, A meta-environment for generating programming environments, ACM Transactions on Software Engineering and Methodology, vol.2, issue.2, pp.176-201, 1993.
DOI : 10.1145/151257.151260
URL : http://hdl.handle.net/11245/1.151564

S. Lucas, Termination of OBJ programs with positive local strategies, Proc. of 2nd International Workshop on Rule-Based Programming, RULE'01, pp.64-78, 2001.

A. Middeldorp and E. Hamoen, Completeness results for basic narrowing, Applicable Algebra in Engineering, Communication and Computing, vol.7, issue.1, pp.213-253, 1994.
DOI : 10.1007/BF01190830

C. G. Nelson and D. C. Oppen, Fast Decision Procedures Based on Congruence Closure, Journal of the ACM, vol.27, issue.2, pp.356-364, 1980.
DOI : 10.1145/322186.322198