. Définition-de-l-'ordre-noethérien-sur-les-clauses-Égalitaires...., 85 5.4.3 Définition de l'ensemble des clauses d'une preuve Spike, p.89

.. Présentation-générale-de-la-tactique-strategiespike, 98 6.1.1 Motivations, p.98

S. La, 118 7.1.1 Motivations, Perspectives : construction interactive des preuves par récurrence implicite à la Spike dans Coq Sommaire 7.1 Présentation générale de l'environnement, p.118

R. and L. B. Akers, Binary Decision Diagrams, IEEE Transactions on Computers, vol.27, issue.6, pp.27509-516, 1978.
DOI : 10.1109/TC.1978.1675141

A. Et-woepcke1853-]-abou-bekr-mohammed-ben-alhacan-al-karkhi and F. Woepcke, Extrait du Fakhri traite d'algebre (manuscript 952, supplement arabe de la Bibliotheque imperiale ) par Abou Bekr Mohammed Ben Alhacan Alkarkhi, 1853.

N. Alvarado, Q. Alvarado, and . Nguyen, ELAN for equational reasoning in Coq, Proceedings of 2nd Workshop on Logical Frameworks and Metalanguages . Institut National de Recherche en Informatique et en Automatique, pp.2-7261, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00107864

N. Baader, T. Baader, and . Nipkow, Term rewriting and all that, 1998.

A. Balaa, Y. Balaa, and . Bertot, Fix-Point Equations for Well-Founded Recursion in Type Theory, Theorem Proving in Higher Order Logics, pp.1-16, 2000.
DOI : 10.1007/3-540-44659-1_1

C. W. Barrett, R. Sebastiani, A. Sanjit, C. Seshia, and . Tinelli, Satisfiability Modulo Theories, Frontiers in Artificial Intelligence and Applications, vol.185, pp.825-885, 2009.
URL : https://hal.archives-ouvertes.fr/hal-01095009

. Barthe, Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant, Functional and Logic Programming, 8th International Symposium, FLOPS 2006 Proceedings, rédacteurs Masami Hagiya et Philip Wadler de Lecture Notes in Computer Science, pp.114-129, 2006.
DOI : 10.1023/A:1019916231463

URL : https://hal.archives-ouvertes.fr/inria-00564237

S. Barthe, S. Barthe, and . Stratulat, Validation of the JavaCard Platform with Implicit Induction Techniques, Proceedings of 14th International Conference, Rewriting Techniques and Applications, RTA 2003 rédacteur Robert Nieuwenhuis, volume 2706 de Lecture Notes in Computer Science, pp.337-351, 2003.
DOI : 10.1007/3-540-44881-0_24

Y. Bertot, P. Bertot, and . Castéran, Interactive theorem proving and program development : Coq'Art : the calculus of inductive constructions, 2004.
DOI : 10.1007/978-3-662-07964-5

URL : https://hal.archives-ouvertes.fr/hal-00344237

. Bezem, Automated Proof Construction in Type Theory Using Resolution, J. Autom. Reasoning, vol.29, pp.3-4253, 2002.
DOI : 10.1007/10721959_10

S. Böhme, T. Böhme, and . Nipkow, Sledgehammer: Judgement Day, Proceedings of 5th International Joint Conference rédacteurs Jürgen Giesl et Reiner Hähnle, pp.107-121, 2010.
DOI : 10.1007/978-3-642-14203-1_9

. Borovanský, An Overview of ELAN, Electronic Notes in Theoretical Computer Science, vol.15, pp.55-70, 1998.
DOI : 10.1016/S1571-0661(05)82552-6

. Bouhoula, Adel Bouhoula, Emmanuel Kounalis et Michaël Rusinowitch, Automated Mathematical Induction. J. Log. Comput, vol.5, issue.5, pp.631-668, 1995.

. Bouhoula, Preuves automatiques par récurrence dans les théories conditionnelles, Thèse de doctorat, 1994.

. Bove, A Brief Overview of Agda -A Functional Language with Dependent Types Theorem Proving in Higher Order Logics, Proceedings of 22nd International Conference de Lecture Notes in Computer Science, pp.73-78, 2009.

M. Boyer, . Boyer, and . Strother-moore, A Computational Logic Handbook, 1988.

M. Boyer, . Boyer, and . Strother-moore, Integrating decision procedures into heuristic theorem provers : a case study of linear arithmetic, pp.83-124, 1988.

[. Braibant, Emancipate yourself from LTac : Your first Coq plugin. http: //gallium.inria.fr/blog/your-first-coq-plugin, p.2012

[. Brassinne, Précis des oeuvres mathématiques de Pierre Fermat et de l

[. 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

R. Samuel and . Buss, Handbook of proof theory, 1998.

R. Samuel and . Buss, An introduction to proof theory. Handbook of proof theory, pp.1-78, 1998.

[. Chlipala, Certified Programming with Dependent Types, 2011.

. Clarke, Clarke, Orna Grumberg et Doron Peled. Model checking, 2001.

. Contejean, Certification of Automated Termination Proofs, Proceedings of 6th International Symposium on Frontiers of Combining Systems, pp.148-162, 2007.
DOI : 10.1007/978-3-540-74621-8_10

URL : https://hal.archives-ouvertes.fr/hal-01125312

[. Contejean, Facettes de la preuve. Habilitation à diriger des recherches, 2014.
URL : https://hal.archives-ouvertes.fr/tel-01089490

H. Coquand and . Huet, The calculus of constructions, Information and Computation, vol.76, issue.2-3, pp.95-120, 1988.
DOI : 10.1016/0890-5401(88)90005-3

URL : https://hal.archives-ouvertes.fr/inria-00076024

[. Corbineau, First-Order Reasoning in the Calculus of Inductive Constructions, Lecture Notes in Computer Science, vol.3085, pp.162-177, 2003.
DOI : 10.1007/978-3-540-24849-1_11

. Courant, Proof reconstruction. Rapport technique, LIP, 1996.

[. Delahaye, A Tactic Language for the System Coq Logic for Programming and Automated Reasoning, Proceedings of 7th International Conference, pp.85-95, 1955.

[. 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

[. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic, The Journal of Symbolic Logic, vol.475, issue.03, pp.795-807, 1992.
DOI : 10.1007/3-540-54487-9_58

[. Gentzen, Untersuchungen ???ber das logische Schlie???en. I, Mathematische Zeitschrift, vol.39, issue.1, pp.176-210, 1935.
DOI : 10.1007/BF01201353

. Gordon, Edinburgh LCF : a mechanized logic of computation, Lecture Notes in Computer Science, vol.78, 1979.
DOI : 10.1007/3-540-09724-4

J. C. Michael and . Gordon, Reachability Programming in HOL98 Using BDDs Theorem Proving in Higher Order Logics, Proceedings of 13th International Conference rédacteurs Mark Aagaard et John Harrison, volume 1869 de Lecture Notes in Computer Science, pp.179-196, 2000.

[. 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

S. Henaien, S. Henaien, and . Stratulat, Performing Implicit Induction Reasoning with Certifying Proof Environments, Proceedings of 4th International Symposium on Symbolic Computation in Software Science, pp.15-17, 2012.
DOI : 10.1093/jigpal/12.1.1

URL : https://hal.archives-ouvertes.fr/hal-00764909

N. Hickey, A. Hickey, and . Nogin, Fast Tactic-Based Theorem Proving Theorem Proving in Higher Order Logics, Proceedings of 13th International Conference rédacteurs Mark Aagaard et John Harrison, volume 1869 de Lecture Notes in Computer Science, pp.252-267, 2000.

[. Howard, The formulas-as-types notion of construction Curry : Essays on Combinatory Logic, Lambda Calculus, and Formalism, J. P. Seldin et J. R. Hindley, pp.479-490, 1980.

J. Hurd, . Integrating, and H. Gandalf, Integrating Gandalf and HOL, Proceedings 12th International Conference Theorem Proving in Higher Order Logics, TPHOLs'99, pp.311-322, 1999.
DOI : 10.1007/3-540-48256-3_21

J. Hurd, First-order proof tactics in higher-order logic theorem provers. Design and Application of Strategies/Tactics in Higher Order Logics, number NASA/CP-2003-212448 in NASA Technical Reports, pp.56-68, 2003.

S. Hutter, C. Hutter, and . Sengler, INKA : The Next Generation. Dans Automated Deduction -CADE-13, Proceedings of 13th International Conference on Automated Deduction, pp.288-292, 1996.

[. Kaliszyk, Validation des preuves par récurrence implicite avec des outils basés sur le calcul des constructions inductives, 2005.

S. Kanso, A. Kanso, and . Setzer, Integrating automated and interactive theorem proving in type theory, AVOCS, vol.2, 2010.

[. Kanso, Agda as a platform for the development of verified railway interlocking systems, Thèse de doctorat, 2012.

. Klein, seL4, Communications of the ACM, vol.53, issue.6, pp.53107-115, 2010.
DOI : 10.1145/1743546.1743574

. Knuth, E. Donald, . Knuth, B. Peter, and . Bendix, Simple Word Problems in Universal Algebras, Automation of Reasoning, pp.342-376, 1983.
DOI : 10.1007/978-3-642-81955-1_23

R. Kounalis and . Kounalis, Mechanizing inductive reasoning, Bulletin of the EATCS, vol.41, pp.216-226, 1990.

[. Kreitz, The Nuprl Proof Development System, Version 5 : Reference Manual and User's Guide, 2002.

. Leroy, Didier Rémy et Jérôme Vouillon. The OCaml system release 4, p.2, 2014.

P. Mccarthy, J. Mccarthy, and . Painter, Correctness of a compiler for arithmetic expressions, Mathematical aspects of computer science, vol.1, 1967.
DOI : 10.1090/psapm/019/0242403

[. Mccarthy, A basis for a mathematical theory of computation, Studies in Logic and the Foundations of Mathematics, pp.33-70, 1959.

. Meng, Automation for interactive proof: First prototype, Information and Computation, vol.204, issue.10, pp.1575-1596, 2006.
DOI : 10.1016/j.ic.2005.05.010

R. David and . Musser, On Proving Inductive Properties of Abstract Data Types, Conference Record of the Seventh Annual ACM Symposium on Principles of Programming Languages, pp.154-162, 1980.

. Owre, User Guide for the PVS Specification and Verification System (Beta Release), 1993.

L. Pascal, L. Pascal, and . Lafuma, Pascal : oeuvres complètes, 1963.

. Paulin-mohring1993-]-christine-paulin-mohring, Inductive definitions in the system Coq rules and properties, Proceedings of International Conference on Typed Lambda Calculi and Applications, TLCA '93, pp.328-345, 1993.
DOI : 10.1007/BFb0037116

[. Peano, Formulaire de mathématiques, Bocca frères, vol.5, 1908.

[. Poincaré, La science et l'hypothèse, Science, vol.6, pp.1-13, 1898.

[. Protzen, Lazy generation of induction hypotheses, Proceedings of 12th International Conference on Automated Deduction, pp.42-56, 1994.
DOI : 10.1007/3-540-58156-1_4

. Rusinowitch, Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm, Proceedings of 12th International Conference, Computer Aided Verification, pp.344-357, 2000.
DOI : 10.1007/10722167_27

URL : https://hal.archives-ouvertes.fr/inria-00099167

. Rusinowitch, Michaël Rusinowitch, Sorin Stratulat et Francis Klay Mechanical verification of an ideal incremental ABR conformance algorithm, J. Autom. Reasoning, vol.30, issue.2, pp.53-177, 2003.

. Schmitt, JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants, Proceedings of 1st International Joint Conference, Automated Reasoning, 2001.
DOI : 10.1007/3-540-45744-5_34

[. Stratulat, Preuves par récurrence avec ensembles couvrants contextuels. Applications á la vérification de logiciels de télécommunications, Thèse de doctorat, 2000.

[. 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

[. Sutcliffe, The CADE-16 ATP System Competition, Journal of Automated Reasoning, vol.24, issue.3, pp.371-396, 2000.
DOI : 10.1023/A:1006393501098

[. Szabo, The collected papers of Gerhard Gentzen, 1969.

. Tammet, . J. Gandalf, and . Autom, Reasoning [The HOL development team] The HOL development team. The HOL System TUTORIAL. http://hol.sourceforge.net/. [The ISABELLE development team] The ISABELLE development team. ISABELLE. http: //isabelle.in.tum.de/. [The PROOFTREE development team] The PROOFTREE development team. PROOFTREE. http://askra.de/software/prooftree/. [The PVS development team] The PVS development team, pp.199-204, 1997.

. Voicu-et-li2009-]-razvan, M. Voicu, and . Li, Descente infinie proofs in Coq, Proceedings of the 1st Coq Workshop, 2009.

C. Wirth, Descente Infinie + Deduction, Logic Journal of IGPL, vol.12, issue.1, pp.1-96, 2004.
DOI : 10.1093/jigpal/12.1.1