A. S. Autexier, D. Hutter, H. Mantel, and A. Schairer, System Description: inka 5.0 - A Logic Voyager, Proceedings of the 16th International Conference on Automated Deduction (CADE-16), volume 1632 of LNAI, pp.207-211, 1999.
DOI : 10.1007/3-540-48660-7_15

A. T. Aoto, Dealing with Non-orientable Equations in Rewriting Induction
DOI : 10.1007/11805618_18

N. Berregeb, A. Bouhoula, and M. Rusinowitch, Automated verification by induction with associative-commutative operators
DOI : 10.1007/3-540-61474-5_71

B. Y. Bertot and P. Casteran, Interactive Theorem Proving and Program Development, 2004.
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237

. N. Ber97 and . Berregeb, Preuves par induction implicite : cas des théories associativescommutatives et observationnelles, Thèse de Doctorat d'Université, 1997.

P. Brauner, C. Houtmann, and C. Kirchner, Principles of Superdeduction, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), pp.41-50, 2007.
DOI : 10.1109/LICS.2007.37
URL : https://hal.archives-ouvertes.fr/inria-00133557

F. Nahon, C. Kirchner, B. A. Héì-ene-kirchner, E. Bouhoula, M. Kounalis et al., Spike: An automatic theorem prover, Proceedings of the 1st International Conference on Logic Programming and Automated Reasoning, St. Petersburg (Russia), pp.460-462, 1992.

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

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

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/inria-00098847

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/hal-01199506

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

J. J. , -. Jouannaud, H. Kirchner, K. C. Kirchner, and H. Kirchner, Completion of a set of rules modulo a set of equations Rewriting, solving, proving. A preliminary version of a book available at www, SIAM Journal of Computing, vol.15, issue.4 3, pp.1155-1194, 1986.

C. Kirchner, H. Kirchner, F. Nahon, K. M. Kaufmann, and J. S. Moore, Narrowing Based Inductive Proof Search, Compass'96: Eleventh Annual Conference on Computer Assurance National Institute of Standards and Technology. 1 KZ95. D. Kapur and H. Zhang. An overview of rewrite rule laboratory (RRL). J. Computer and Mathematics with Applications, pp.91-114, 1995.
DOI : 10.1007/s10472-009-9154-5
URL : https://hal.archives-ouvertes.fr/hal-00692193

M. C. Marché, Réécriture modulo une théorie présentée par un système convergent et décidabilité duprobì eme du mot dans certaines classes de théories théorieséquationnelles, Thèse de, p.11, 1993.

N. F. Nahon, Preuves par induction dans le calcul des séquents modulo, p.11, 2007.

T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL ? A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS Complete sets of reductions for some equational theories, Journal of the ACM, vol.28, issue.2, pp.233-264, 1981.

R. U. Reddy, Term rewriting induction, Proceedings 10th International Conference on Automated Deduction, pp.162-177, 1990.
DOI : 10.1007/3-540-52885-7_86