T. Aoto, Dealing with Non-orientable Equations in Rewriting Induction, Lecture Notes in Computer Science, vol.4098, pp.242-256, 2006.
DOI : 10.1007/11805618_18

R. Aubin, Mechanizing structural induction part I: Formal system, Theoretical Computer Science, vol.9, issue.3, pp.329-362, 1979.
DOI : 10.1016/0304-3975(79)90034-3

J. Avenhaus, U. Kühler, T. Schmidt-samoa, and C. Wirth, How to Prove Inductive Theorems? QuodLibet!, Proceedings of the 19th International Conference on Automated Deduction (CADE-19), number 2741 in Lecture Notes in Artificial Intelligence, pp.328-333, 2003.
DOI : 10.1007/978-3-540-45085-6_29

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

L. Bachmair, Proof by consistency in equational theories Logic in Computer Science, LICS '88 Proceedings of the Third Annual Symposium on, pp.228-233, 1988.

A. Bouhoula, E. Kounalis, and M. Rusinowitch, SPIKE, an automatic theorem prover, Logic Programming and Automated Reasoning (LPAR), pp.460-462, 1992.
DOI : 10.1007/BFb0013087

A. Bouhoula, E. Kounalis, and M. Rusinowitch, Automated Mathematical Induction, Journal of Logic and Computation, vol.5, issue.5, pp.631-668, 1995.
DOI : 10.1093/logcom/5.5.631
URL : https://hal.archives-ouvertes.fr/inria-00074484

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

R. Boulton and K. Slind, Automatic Derivation and Application of Induction Schemes for Mutually Recursive Functions, Computational Logic ? CL, pp.629-643, 2000.
DOI : 10.1007/3-540-44957-4_42

R. S. Boyer and J. S. Moore, A Computational Logic, 1979.

R. S. Boyer and J. S. Moore, A computational logic handbook, 1988.

F. Bronsard and U. S. Reddy, Conditional rewriting in focus, Conditional and Typed Rewriting Systems, pp.1-13, 1991.
DOI : 10.1007/3-540-54317-1_77

F. Bronsard, U. S. Reddy, and R. Hasker, Induction using term orderings, Automated Deduction ?CADE-12, pp.102-117, 1994.
DOI : 10.1007/3-540-58156-1_8

J. Brotherston and A. Simpson, Sequent calculi for induction and infinite descent, Journal of Logic and Computation, vol.21, issue.6, 2010.
DOI : 10.1093/logcom/exq052

R. M. Burstall, Proving Properties of Programs by Structural Induction, The Computer Journal, vol.12, issue.1, pp.41-48, 1969.
DOI : 10.1093/comjnl/12.1.41

H. Comon, Inductionless Induction, Handbook of Automated Reasoning, pp.913-962, 2001.
DOI : 10.1016/B978-044450813-3/50016-3

H. Comon and R. Nieuwenhuis, Induction= I-axiomatization+ first-order consistency. Information and computation(Print), pp.151-186, 2000.

J. Courant, Proof reconstruction Research Report RR96-26, LIP, 1996. Preliminary version. [19] N. Dershowitz. Applications of the Knuth-Bendix completion procedure, Seminaire d'Informatique Theorique, pp.95-111, 1982.

N. Dershowitz and U. S. Reddy, Deductive and inductive synthesis of equational programs, Journal of Symbolic Computation, vol.15, issue.5-6, pp.467-494, 1993.
DOI : 10.1016/S0747-7171(06)80002-7

L. Fribourg, A Strong restriction of the inductive completion procedure, ICALP (International Conference on Automata, Languages and Programming)Extended version in Journal of Symbolic Computation, pp.105-115, 1986.
DOI : 10.1007/3-540-16761-7_60

S. J. Garland and J. V. Guttag, Inductive methods for reasoning about abstract data types, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '88, pp.219-228, 1988.
DOI : 10.1145/73560.73579

J. Goguen, How to prove algebraic inductive hypotheses without induction, 5th Conference on Automated Deduction (CADE05), pp.356-373, 1980.
DOI : 10.1007/3-540-10009-1_27

B. Gramlich, Strategic Issues, Problems and Challenges in Inductive Theorem Proving, Electronic Notes in Theoretical Computer Science, vol.125, issue.2, pp.5-43, 2005.
DOI : 10.1016/j.entcs.2005.01.006

G. Huet and J. M. Hullot, Proofs by induction in equational theories with constructors, 1980.
URL : https://hal.archives-ouvertes.fr/inria-00076533

J. Jouannaud and E. Kounalis, Automatic proofs by induction in equational theories without constructors, Proceedings of the First Annual IEEE Symp. on Logic in Computer Science, LICS 1986, pp.358-366, 1986.

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, 8th International Conference on Automated Deduction, pp.99-117, 1986.
DOI : 10.1007/3-540-16780-3_83

D. Kapur and M. Subramaniam, Automating induction over mutually recursive functions, Algebraic Methodology and Software Technology, pp.117-131, 1996.
DOI : 10.1007/BFb0014311

D. Kapur and H. Zhang, Automating induction: Explicit vs. inductionless, Proc. Third International Symposium on Artificial Intelligence and Mathematics, pp.2-5, 1994.

S. C. Kleene, General recursive functions of natural numbers, Mathematische Annalen, vol.110, issue.1, pp.727-742, 1936.
DOI : 10.1007/BF01565439

D. E. Knuth and P. B. Bendix, Simple Word Problems in Universal Algebras, Computational Problems in Abstract Algebra, pp.263-297, 1970.
DOI : 10.1007/978-3-642-81955-1_23

E. Kounalis and M. Rusinowitch, A mechanization of conditional reasoning, First International Symposium on Artificial Intelligence and Mathematics, 1990.

E. Kounalis and M. Rusinowitch, Mechanizing inductive reasoning, Proceedings of the eighth National conference on Artificial intelligence AAAI'90, pp.240-245, 1990.

W. Küchlin, Inductive Completion by Ground Proof Transformation, Resolution of Equations in Algebraic Structures (Volume II): Rewriting Techniques, pp.211-244, 1989.
DOI : 10.1016/B978-0-12-046371-8.50013-4

D. Lankford, Some remarks on inductionless induction, Math. Dept., Louisiana Tech. Univ, 1980.

J. Mccarthy, A basis for a mathematical theory of computation, Computer Programming and Formal Systems, pp.33-70, 1963.

J. Mccarthy and J. Painter, Correctness of a compiler for arithmetic expressions, Mathematical Aspects of Computer Science, pp.33-41, 1967.
DOI : 10.1090/psapm/019/0242403

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

D. Naidich, On generic representation of implicit induction procedures, 1996.

M. Protzen, Lazy generation of induction hypotheses Automated Deduction ?CADE-12, pp.42-56, 1994.

C. Rabadan and F. Klay, Un nouvel algorithme de contrôle de conformité pour la capacité de transfert 'Available Bit Rate, 1997.

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

M. Rusinowitch, S. Stratulat, and F. Klay, Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm, J. Autom. Reasoning, vol.30, issue.2, pp.53-177, 2003.
DOI : 10.1007/10722167_27
URL : https://hal.archives-ouvertes.fr/inria-00099167

C. Sprenger and M. Dam, On the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in the ??Calculus, Foundations of Software Science and Computation Structures, pp.425-440, 2003.
DOI : 10.1007/3-540-36576-1_27

S. Stratulat, A General Framework to Build Contextual Cover Set Induction Provers, Journal of Symbolic Computation, vol.32, issue.4, pp.403-445, 2001.
DOI : 10.1006/jsco.2000.0469
URL : https://hal.archives-ouvertes.fr/inria-00100927

S. Stratulat, Automatic ???Descente Infinie??? Induction Reasoning, Lecture Notes in Artificial Intelligence, vol.3702, pp.262-276, 2005.
DOI : 10.1007/11554554_20

S. Stratulat, 'Descente Infinie' Induction-Based Saturation Procedures, Ninth International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2007), pp.17-24, 2007.
DOI : 10.1109/SYNASC.2007.17

S. Stratulat, Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities, Rewriting Techniques and Applications, pp.351-365, 2008.
DOI : 10.1007/978-3-540-70590-1_24

S. Stratulat, Integrating Implicit Induction Proofs into Certified Proof Environments, Integrated Formal Methods, pp.320-335, 2010.
DOI : 10.1007/978-3-540-70590-1_24
URL : https://hal.archives-ouvertes.fr/hal-00553070

S. Stratulat, Making explicit the implicit induction. submitted, 2012.

S. Stratulat and V. Demange, Automated Certification of Implicit Induction Proofs, CPP'2011 (First International Conference on Certified Programs and Proofs), pp.37-53, 2011.
DOI : 10.1007/978-3-642-16265-7_23
URL : https://hal.archives-ouvertes.fr/hal-00644876

A. Turing, On computable numbers, with an application to the Entscheidungsproblem, Proceedings of the, pp.230-265, 1936.

C. Walther, Mathematical induction, Handbook of Logic in Artificial Intelligence and Logic Programming, pp.127-228, 1994.

C. Wirth, History and future of implicit and inductionless induction: Beware the old jade and the zombie ! In Mechanizing Mathematical Reasoning: Essays in Honor of Jörg H. Siekmann on the Occasion of His 60th Birthday, number 2605 in Lecture Notes in Artificial Intelligence, pp.192-203, 2005.

C. Wirth and B. Gramlich, On notions of inductive validity for first-order equational clauses. Automated Deduction ?CADE-12, pp.162-176, 1994.

H. Zhang, D. Kapur, and M. S. Krishnamoorthy, A mechanizable induction principle for equational specifications, Proceedings of the 9th International Conference on Automated Deduction, pp.162-181, 1988.
DOI : 10.1007/BFb0012831