F. Baader and T. Nipkow, Term Rewriting and all That, 1998.

G. Barthe, H. Cirstea, C. Kirchner, and L. Liquori, Pure Patterns Type Systems, Principles of Programming Languages -POPL2003, 2003.
URL : https://hal.archives-ouvertes.fr/inria-00099463

N. Berregeb, A. Bouhoula, and M. Rusinowitch, SPIKE-AC: A system for proofs by induction in Associative-Commutative theories, Rewriting Techniques and Applications, RTA'96, pp.428-431, 1996.
DOI : 10.1007/3-540-61464-8_73

A. Bouhoula, E. Kounalis, and M. Rusinowitch, SPIKE, an automatic theorem prover, Proceedings of the 1st International Conference on Logic Programming and Automated Reasoning, St. Petersburg (Russia), pp.460-462, 1992.
DOI : 10.1007/BFb0013087

A. Bundy, D. Basin, D. Hutter, and A. Ireland, Rippling: Meta-Level Guidance for Mathematical Reasoning, 2005.
DOI : 10.1017/CBO9780511543326

H. Comon and R. Nieuwenhuis, Induction=I-Axiomatization+First-Order Consistency, Information and Computation, vol.159, issue.1-2, pp.151-186, 2000.
DOI : 10.1006/inco.2000.2875

E. Deplagne, Système de preuve modulo récurrence, Thèse de doctorat, 2002.

E. Deplagne and C. Kirchner, Induction as deduction modulo, 2004.
URL : https://hal.archives-ouvertes.fr/inria-00099871

E. Deplagne, C. Kirchner, H. Kirchner, and Q. Nguyen, Proof Search and Proof Check for Equational and Inductive Theorems, Proceedings of CADE-19, 2003.
DOI : 10.1007/978-3-540-45085-6_26
URL : https://hal.archives-ouvertes.fr/inria-00099470

G. Dowek, La part du Calcul, 1999.

G. Dowek, T. Hardin, and C. Kirchner, HOL-????: an intentional first-order expression of higher-order logic, Mathematical Structures in Computer Science, vol.11, issue.1, pp.21-45, 2001.
DOI : 10.1017/S0960129500003236
URL : https://hal.archives-ouvertes.fr/hal-01199524

G. Dowek, T. Hardin, and C. Kirchner, Theorem proving modulo, Journal of Automated Reasoning, vol.31, issue.1, pp.33-72, 2003.
DOI : 10.1023/A:1027357912519
URL : https://hal.archives-ouvertes.fr/inria-00077199

M. Ferreira, Termination of Term Rewriting: Well foundedness, Totality and Transformations, 1995.

H. Ganzinger and J. Stuber, Inductive theorem proving by consistency for firstorder clauses, Conditional Term Rewriting Systems, Third International Workshop, pp.226-241, 1992.

J. Girard, Y. Lafont, and P. Taylor, Proofs and Types, volume 7 of Cambridge Tracts in Theoretical Computer Science, 1989.

G. Huet, Constrained Resolution: A Complete Method for Higher Order Logic, 1972.

J. Hullot, Canonical forms and unification, Proceedings 5th International Conference on Automated Deduction, Les Arcs (France), pp.318-334, 1980.
DOI : 10.1007/3-540-10009-1_25

D. Kapur and H. Zhang, An overview of Rewrite Rule Laboratory (RRL), Computers & Mathematics with Applications, vol.29, issue.2, pp.91-114, 1995.
DOI : 10.1016/0898-1221(94)00218-A

C. Kirchner and H. Kirchner, Rewriting, solving, proving. A preliminary version of a book available at www, 1999.

C. Kirchner, H. Kirchner, and M. Rusinowitch, Deduction with symbolic constraints . Revue d'Intelligence Artificielle, pp.9-52, 1990.
URL : https://hal.archives-ouvertes.fr/inria-00077103

D. Musser, On proving inductive properties of abstract data types, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '80, 1980.
DOI : 10.1145/567446.567461

F. Nahon, Preuve par induction dans le calcul des séquents modulo, 2007.

F. Nahon, C. Kirchner, H. Kirchner, and P. Brauner, Inductive proof search modulo, Annals of Mathematics and Artificial Intelligence, vol.28, issue.6, pp.123-154, 2009.
DOI : 10.1007/s10472-009-9154-5
URL : https://hal.archives-ouvertes.fr/inria-00337380

G. Steel, Proof by consistency -a literature survey, 1999.

B. Wack, Typage et déduction dans le calcul de réécriture, Thèse de doctorat, 2005.