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. Jacquemard, Automated Induction with Constrained Tree Automata, Proc. of the 4th International Joint Conference on Automated Reasoning (IJCAR), pp.539-554, 2008.
DOI : 10.1007/978-3-540-71070-7_44
URL : https://hal.archives-ouvertes.fr/inria-00579004

A. Bouhoula and J. Jouannaud, Automata-Driven Automated Induction, Information and Computation, vol.169, issue.1, pp.1-22, 2001.
DOI : 10.1006/inco.2001.3036

A. Bouhoula, J. Jouannaud, and J. Meseguer, Specification and proof in membership equational logic, Theoretical Computer Science, vol.236, issue.1-2, pp.35-132, 2000.
DOI : 10.1016/S0304-3975(99)00206-6
URL : https://hal.archives-ouvertes.fr/inria-00099079

A. Bouhoula and M. Rusinowitch, Implicit induction in conditional theories, Journal of Automated Reasoning, vol.31, issue.2, 1995.
DOI : 10.1007/BF00881856
URL : https://hal.archives-ouvertes.fr/inria-00074627

M. Dauchet, A. Caron, and J. Coquidé, Automata for Reduction Properties Solving, Journal of Symbolic Computation, vol.20, issue.2, pp.215-233, 1995.
DOI : 10.1006/jsco.1995.1048

H. Comon, Sufficient completeness, term rewriting systems and ???anti-unification???
DOI : 10.1007/3-540-16780-3_85

H. Comon and V. Cortier, Tree automata with one memory set constraints and cryptographic protocols, Theoretical Computer Science, vol.331, issue.1, pp.143-214, 2005.
DOI : 10.1016/j.tcs.2004.09.036
URL : https://hal.archives-ouvertes.fr/inria-00000553

H. Comon and F. Jacquemard, Ground reducibility is exptime-complete. Information and Computation, pp.123-153, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00578859

E. Contejean, C. March, B. Monate, and X. Urbain, Proving termination of rewriting with cime, ext. abstracts of the 6th Int. Workshop on Termination, WST'03, pp.71-73, 2003.

N. Dershowitz and J. Jouannaud, Rewrite Systems, Formal Models and Sematics, pp.243-320, 1990.
DOI : 10.1016/B978-0-444-88074-1.50011-1

N. Dershowitz, M. Okada, and G. Sivakumar, Confluence of conditional rewrite systems, Proc. 1st International Workshop on Conditional Term Rewriting Systems, pp.31-44, 1987.
DOI : 10.1007/3-540-19242-5_3

F. Durán, S. Lucas, J. Meseguer, and M. , MTT: The Maude Termination Tool (System Description), Proc. of the 4th International Joint Conference on Automated Reasoning (IJCAR 08), pp.313-319, 2008.
DOI : 10.1007/978-3-540-71070-7_27

H. Ganzinger, Ground term confluence in parametric conditional equational specifications, Proc. STACS, pp.286-298, 1987.
DOI : 10.1007/BFb0039613

J. Giesl, P. Schneider-kamp, and R. , Thiemann AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework, Proc. of the third International Joint Conference on Automated Reasoning (IJCAR '06), pp.281-286, 2006.

I. Gnaedig and H. Kirchner, Computing constructor forms with non terminating rewrite programs, Proceedings of the 8th ACM SIGPLAN symposium on Principles and practice of declarative programming , PPDP '06, pp.121-132, 2006.
DOI : 10.1145/1140335.1140351
URL : https://hal.archives-ouvertes.fr/inria-00112083

J. V. Guttag, The Specification and Application to Programming of Abstracta Data Types, 1975.

J. V. Guttag, Notes on type abstraction, Program Construction, pp.593-616, 1978.
DOI : 10.1007/BFb0014684

J. V. Guttag and J. J. Horning, The algebraic specification of abstract data types, Acta Informatica, vol.10, pp.27-52, 1978.

J. Hendrix, M. Clavel, and J. Meseguer, A Sufficient Completeness Reasoning Tool for Partial Specifications, Proc. ot the 16th Int. Conf. on Term Rewriting and Applications (RTA), pp.165-174, 2005.
DOI : 10.1007/978-3-540-32033-3_13

J. Hendrix, H. Ohsaki, and J. Meseguer, Sufficient completeness checking with propositional tree automata, UILU-ENG-2005-1825 (ENGR), 2005.

G. Huet and J. Hullot, Proofs by induction in equational theories with constructors, Journal of Computer and System Sciences, vol.25, issue.2, pp.239-266, 1982.
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 Equational Theories Without Constructors, Proc. of the 1st Symposium on Logic in Computer Science (LICS), pp.358-366, 1986.

S. Kaplan, Simplifying conditional term rewriting systems : Unification, termination and confluence, Journal of Symbolic Computation, vol.4, issue.3, pp.295-334, 1987.
DOI : 10.1016/S0747-7171(87)80010-X

D. Kapur, An automated tool for analyzing completeness of equational specifications, Proceedings of the 1994 international symposium on Software testing and analysis , ISSTA '94, pp.28-43, 1994.
DOI : 10.1145/186258.186496

D. Kapur, P. Narendan, and F. Otto, On ground-confluence of term rewriting systems, Information and Computation, vol.86, issue.1, pp.14-31, 1990.
DOI : 10.1016/0890-5401(90)90023-B

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

D. Kapur, P. Narendran, D. J. Rosenkrantz, and H. Zhang, Sufficient-completeness, ground-reducibility and their complexity, Acta Informatica, vol.65, issue.4, pp.311-350, 1991.
DOI : 10.1007/BF01893885

M. Korp, C. Sternagel, H. Zankl, and A. Middeldorp, Tyrolean Termination Tool 2, Proc. of the Int. Conf. on Rewriting Techniques and Applications (RTA), pp.295-304, 2009.
DOI : 10.1007/978-3-540-70590-1_23

E. Kounalis, Completeness in data type specifications, European Conference on Computer Algebra, pp.348-362, 1985.

E. Kounalis and M. Rusinowitch, Studies on the ground convergence property of conditional theories, Proc. AMAST Workshop in Computing, pp.363-376, 1992.

A. Lazrek, P. Lescanne, and J. Thiel, Tools for proving inductive equalities, relative completeness, and ??-completeness, Information and Computation, vol.84, issue.1, pp.47-70, 1990.
DOI : 10.1016/0890-5401(90)90033-E

S. Lucas and . Mu-term, A Tool for Proving Termination of Context-Sensitive Rewriting, Proc. of 15th Int. Conf. on Rewriting Techniques and Applications (RTA) 2004 of Springer LNCS, pp.200-209, 2004.

J. Misra, Powerlist: a structure for parallel recursion, ACM Transactions on Programming Languages and Systems, vol.16, issue.6, pp.1737-1767, 1994.
DOI : 10.1145/197320.197356