P. Borovansk´yborovansk´y, C. Kirchner, H. Kirchner, P. Moreau, and C. Ringeissen, An Overview of ELAN, Proceedings of the 2nd International Workshop on Rewriting Logic and its Applications, 1998.

A. Bouhoula, Using induction and rewriting to verify and complete parameterized specifications, Theoretical Computer Science, vol.170, issue.1-2, pp.245-276, 1996.
DOI : 10.1016/S0304-3975(96)80708-0

A. Bouhoula and F. Jaquemard, Automatic verification of. sufficient completeness for. specifications of complex data structures, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00578926

A. Caron, J. Coquide, and M. Dauchet, Encompassment properties and automata with constraints, Proceedings 5th Conference on Rewriting Techniques and Applications, pp.328-342, 1993.
DOI : 10.1007/3-540-56868-9_25

M. Clavel, S. Eker, P. Lincoln, and J. Meseguer, Principles of Maude, Proceedings of the 1st International Workshop on Rewriting Logic and its Applications, 1996.
DOI : 10.1016/S1571-0661(04)00034-9

H. Comon, Sufficient completeness, term rewriting systems and ???anti-unification???, Proceedings 8th International Conference on Automated Deduction, pp.128-140, 1986.
DOI : 10.1007/3-540-16780-3_85

H. Comon, Inductionless Induction, Handbook of Automated Reasoning, pp.913-962, 2001.
DOI : 10.1016/B978-044450813-3/50016-3
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.53.5750

H. Comon and F. Jacquemard, Ground reducibility is EXPTIME-complete, Proc. 12th IEEE Symp. Logic in Computer Science, pp.26-34, 1997.
URL : https://hal.archives-ouvertes.fr/inria-00578859

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, Outermost Ground Termination, Proceedings of the 4th 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

O. Fissore, I. Gnaedig, and H. Kirchner, A Proof of Weak Termination Providing the Right Way to Terminate, 1st International Colloquium on THEORETICAL ASPECTS OF COMPUTING, pp.356-371, 2004.
DOI : 10.1007/978-3-540-31862-0_26
URL : https://hal.archives-ouvertes.fr/inria-00100120

O. Fissore, I. Gnaedig, and H. Kirchner, Proving weak termination also provides the right way to terminate -Extended version, 2004.
URL : https://hal.archives-ouvertes.fr/inria-00107744

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

J. Giesl, R. Thiemann, P. Schneider-kamp, and S. Falke, Improving Dependency Pairs, Proceedings of the 10th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR '03), pp.165-179, 2003.
DOI : 10.1007/978-3-540-39813-4_11

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

G. Huet and J. Hullot, Proofs by induction in equational theories with constructors, Preliminary version in Proceedings 21st Symposium on Foundations of Computer Science, pp.239-266, 1980.
DOI : 10.1016/0022-0000(82)90006-X
URL : https://hal.archives-ouvertes.fr/inria-00076533

J. Jouannaud and E. Kounalis, Automatic proofs by induction in theories without constructors, Information and Computation, vol.82, issue.1, pp.1-33, 1989.
DOI : 10.1016/0890-5401(89)90062-X

D. Kapur, P. Narendran, and H. Zhang, Proof by induction using test sets, Proceedings 8th International Conference on Automated Deduction, pp.99-117, 1986.
DOI : 10.1007/3-540-16780-3_83

D. Kapur, P. Narendran, and H. Zhang, On sufficient-completeness and related properties of term rewriting systems, Acta Informatica, vol.6, issue.5, pp.395-415, 1987.
DOI : 10.1007/BF00292110

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

E. Kounalis, Completeness in data type specifications, Proceedings EUROCAL Conference, Linz (Austria), pp.348-362, 1985.

E. Kounalis, Testing for the ground (co-)reducibility property in term-rewriting systems, Theoretical Computer Science, vol.106, issue.1, pp.87-117, 1992.
DOI : 10.1016/0304-3975(92)90279-O

A. Lazrek, P. Lescanne, and J. Thiel, Tools for proving inductive equalities, relative completeness and ?completeness . Information and Computation, pp.47-70, 1990.

P. Moreau, C. Ringeissen, and M. Vittek, A Pattern Matching Compiler for Multiple Target Languages, 12th Conference on Compiler Construction, pp.61-76, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00099427

T. Nipkow and G. Weikum, A decidability result about sufficient-completeness of axiomatically specified abstract data types, 6th GI Conference, pp.257-268, 1983.
DOI : 10.1007/BFb0036486

D. Plaisted, Semantic confluence tests and completion methods, Information and Control, vol.65, issue.2-3, pp.182-215, 1985.
DOI : 10.1016/S0019-9958(85)80005-X