M. Armand, G. Faure, B. Grégoire, C. Keller, L. Théry et al., A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses, Lecture Notes in Computer Science, vol.53, issue.6, pp.135-150, 2011.
DOI : 10.1145/1217856.1217859
URL : https://hal.archives-ouvertes.fr/hal-00639130

P. Baumgartner and U. Waldmann, Hierarchic Superposition with Weak Abstraction, Lecture Notes in Computer Science, vol.7898, pp.39-57, 2013.
DOI : 10.1007/978-3-642-38574-2_3
URL : https://hal.archives-ouvertes.fr/hal-00931919

C. Jasmin and . Blanchette, Automatic Proofs and Refutations for Higher-order Logic, 2012.

C. Jasmin, S. Blanchette, L. C. Böhme, and . Paulson, Extending Sledgehammer with SMT solvers, J. Autom. Reasoning, vol.51, issue.1, pp.109-128, 2013.

C. Jasmin, S. Blanchette, A. Böhme, N. Popescu, and . Smallbone, Encoding monomorphic and polymorphic types, TACAS, Lecture Notes in Computer Science, pp.493-507, 2013.

C. Jasmin, A. Blanchette, D. Popescu, C. Wand, and . Weidenbach, More SPASS with Isabelle -Superposition with hard sorts and configurable simplification, Lecture Notes in Computer Science, vol.7406, pp.345-360, 2012.

F. Bobot and A. Paskevich, Expressing Polymorphic Types in a Many-Sorted Language, FroCoS, pp.87-102, 2011.
DOI : 10.1007/978-3-540-78800-3_24
URL : https://hal.archives-ouvertes.fr/inria-00591414

S. Böhme, Proving Theorems of Higher-Order Logic with SMT Solvers, 2012.

S. Böhme and T. Weber, Fast LCF-Style Proof Reconstruction for Z3, Interactive Theorem Proving, pp.179-194, 2010.
DOI : 10.1007/978-3-642-14052-5_14

J. Harrison, Optimizing proof search in model elimination, Lecture Notes in Computer Science, vol.1104, pp.313-327, 1996.
DOI : 10.1007/3-540-61511-3_97
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.106.4548

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.

J. Hurd, System description: The Metis proof tactic. Empirically Successful Automated Reasoning in Higher-Order Logic (ESHOL), pp.103-104, 2005.

C. Kaliszyk and J. Urban, MizAR 40 for Mizar 40, Journal of Automated Reasoning, vol.50, issue.1-2, 1310.
DOI : 10.1007/s10817-015-9330-8

C. Kaliszyk and J. Urban, Learning-Assisted Automated Reasoning with Flyspeck, Journal of Automated Reasoning, vol.50, issue.1???2, pp.10817-10831, 2014.
DOI : 10.1007/s10817-014-9303-3
URL : http://arxiv.org/abs/1211.7012

C. Jasmin, C. Blanchette-lawrence, and . Paulson, Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers, 2010.

S. Lescuyer, Formalizing and Implementing a Reflexive Tactic for Automated Deduction in Coq, 2011.
URL : https://hal.archives-ouvertes.fr/tel-00713668

J. Meng and L. C. Paulson, Translating Higher-Order Clauses to First-Order Clauses, Journal of Automated Reasoning, vol.9, issue.2, pp.35-60, 2008.
DOI : 10.1007/s10817-007-9085-y
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.64.573

M. Norrish, Complete Integer Decision Procedures as Derived Rules in HOL, Theorem Proving in Higher Order Logics, pp.71-86, 2003.
DOI : 10.1007/10930755_5
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.83.2209

C. Lawrence and . Paulson, A generic tableau prover and its integration with Isabelle, J. UCS, vol.5, issue.3, pp.73-87, 1999.

G. Sutcliffe, S. Schulz, K. Claessen, and P. Baumgartner, The TPTP Typed First-Order Form with Arithmetic, Lecture Notes in Computer Science, vol.7180, pp.406-419, 2012.
DOI : 10.1007/978-3-642-28717-6_32

J. Urban, Automated reasoning for Mizar: Artificial intelligence through knowledge exchange, LPAR Workshops CEUR Workshop Proceedings. CEUR-WS.org, 2008.

T. Weber, SMT solvers: new oracles for the HOL theorem prover, International Journal on Software Tools for Technology Transfer, vol.7, issue.1, pp.419-429, 2011.
DOI : 10.1007/s10009-011-0188-8