J. Alama, Escape to Mizar from ATPs, EPiC EasyChair, vol.21, pp.3-11, 2013.

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, CPP 2011, pp.135-150, 2011.
DOI : 10.1145/1217856.1217859
URL : https://hal.archives-ouvertes.fr/hal-00639130

S. Autexier, C. Benzmüller, A. Fiedler, H. Horacek, and Q. B. Vo, Assertion-level Proof Representation with Under-Specification, Electronic Notes in Theoretical Computer Science, vol.93, pp.5-23, 2004.
DOI : 10.1016/j.entcs.2003.12.026
URL : http://doi.org/10.1016/j.entcs.2003.12.026

N. Azmy and C. Weidenbach, Computing Tiny Clause Normal Forms, CADE-24, pp.109-125, 2013.
DOI : 10.1007/978-3-642-38574-2_7
URL : https://hal.archives-ouvertes.fr/hal-00931893

L. Bachmair and H. Ganzinger, Resolution Theorem Proving, Handbook of Automated Reasoning, pp.19-99, 2001.
DOI : 10.1016/B978-044450813-3/50004-7

C. Barrett, A. Stump, and C. Tinelli, The SMT-LIB standard?Version 2.0, p.2010, 2010.

C. Benzmüller, L. C. Paulson, F. Theiss, and A. Fietzke, LEO-II?A cooperative automatic theorem prover for higher-order logic, IJCAR 2008, pp.162-170, 2008.

F. Besson, P. Fontaine, and L. Théry, A flexible proof format for SMT: A proposal, pp.15-26, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00642544

J. C. Blanchette, Automatic proofs and refutations for higher-order logic, 2012.

J. C. Blanchette, Redirecting proofs by contradiction, EasyChair, vol.14, pp.11-26, 2013.

J. C. Blanchette, S. Böhme, and L. C. Paulson, Extending Sledgehammer with SMT Solvers, J. Autom. Reasoning, vol.37, issue.1-2, pp.109-128, 2013.
DOI : 10.1007/BFb0028402

J. C. Blanchette, S. Böhme, A. Popescu, and N. Smallbone, Encoding Monomorphic and Polymorphic Types, TACAS 2013, pp.493-507, 2013.
DOI : 10.1007/978-3-642-36742-7_34
URL : http://arxiv.org/abs/1609.08916

J. C. Blanchette, A. Popescu, D. Wand, and C. Weidenbach, More SPASS with Isabelle?Superposition with hard sorts and configurable simplification, ITP 2012, pp.345-360, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00760392

S. Böhme, Proving theorems of higher-order logic with SMT solvers, 2012.

S. Böhme and T. Nipkow, Sledgehammer: Judgement Day, IJCAR 2010, pp.107-121, 2010.
DOI : 10.1007/978-3-642-14203-1_9

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

T. Bouton, D. C. De-oliveira, D. Déharbe, and P. Fontaine, veriT: An open, trustable and efficient SMTsolver, CADE-22, pp.151-156, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00430634

A. R. Bradley and Z. Manna, Property-directed incremental invariant generation. Formal Asp, Comput, vol.20, pp.379-405, 2008.
DOI : 10.1007/s00165-008-0080-9

C. E. Brown, Satallax: An Automatic Higher-Order Prover, IJCAR 2012, pp.111-117, 2012.
DOI : 10.1007/978-3-642-31365-3_11

C. E. Brown, Using Satallax to generate proof terms for conjectures in Coq, 2012.

M. Caminati, Re: [isabelle] sledgehammer, smt and metis. https://lists.cam.ac.uk/pipermail/ cl-isabelle-users, 2014.

A. Chaieb and T. Nipkow, Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic, LPAR 2005, pp.367-380, 2005.
DOI : 10.1007/11591191_26
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.69.2064

A. Church, A formulation of the simple theory of types, The Journal of Symbolic Logic, vol.1, issue.02, pp.56-68, 1940.
DOI : 10.2307/2371199

B. I. Dahn, Robbins Algebras Are Boolean: A Revision of McCune's Computer-Generated Solution of Robbins Problem, Journal of Algebra, vol.208, issue.2, pp.526-532, 1998.
DOI : 10.1006/jabr.1998.7467

M. Davis, Obvious logical inferences, IJCAI '81, pp.530-531, 1981.

C. Diekmann, Network security policy verification Archive of Formal Proofs, 2014.

M. Fleury, Translation of proofs provided by external provers Internship report, 2014.

S. Foster and G. Struth, Regular algebras Archive of Formal Proofs, 2014.

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

M. J. Gordon and T. F. Melham, Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, 1993.

J. Herbrand, Thèses présentées à la faculté des sciences de paris pour obtenir le grade de docteur ès sciences mathématiques, 1930.

T. Hillenbrand, A. Buch, R. Vogt, and B. Löchner, WALDMEISTER?High-performance equational deduction, Journal of Automated Reasoning, vol.18, issue.2, pp.265-270, 1997.
DOI : 10.1023/A:1005872405899

K. Hoder, L. Kovacs, and A. Voronkov, Vampire usage and demo. Presentation at the Vampire tutorial at CADE-23, 2011.

X. Huang, Translating machine-generated resolution proofs into ND-proofs at the assertion level, PRICAI '96, pp.399-410, 1996.
DOI : 10.1007/3-540-61532-6_34

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

S. Ja´skowskija´skowski, On the rules of suppositions in formal logic, Studia Logica, vol.1, pp.5-32, 1934.

C. Kaliszyk and J. Urban, PRocH: Proof Reconstruction for HOL Light, CADE-24, pp.267-273, 2013.
DOI : 10.1007/978-3-642-38574-2_18

C. Kaliszyk and J. Urban, Learning-Assisted Automated Reasoning with Flyspeck, Journal of Automated Reasoning, vol.50, issue.1???2, pp.173-213, 2014.
DOI : 10.1007/s10817-014-9303-3

R. M. Karp, Reducibility among combinatorial problems, Complexity of Computer Computations, IBM Research Symposia Series, pp.85-103, 1972.
DOI : 10.1007/978-3-540-68279-0_8

G. Klein, T. Nipkow, and L. Paulson, Archive of Formal Proofs

D. Kühlwein, J. C. Blanchette, C. Kaliszyk, and J. Urban, MaSh: Machine Learning for Sledgehammer, ITP 2013, pp.35-50, 2013.
DOI : 10.1007/978-3-642-39634-2_6

D. W. Loveland, Automated Theorem Proving: A Logical Basis, 1978.

R. Matuszewski and P. Rudnicki, Mizar: The first 30 years, Mechanized Mathematics and Its Applications, vol.4, issue.1, pp.3-24, 2005.

A. Meier, System Description: Tramp: Transformation of Machine-Found Proofs into Natural Deduction Proofs at the Assertion Level, CADE-17, pp.460-464, 2000.
DOI : 10.1007/10721959_37

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

J. Meng and L. C. Paulson, Lightweight relevance filtering for machine-generated resolution problems, Journal of Applied Logic, vol.7, issue.1, pp.41-57, 2009.
DOI : 10.1016/j.jal.2007.07.004

D. Miller and A. Felty, An integration of resolution and natural deduction theorem proving, AAAI-86, pp.198-202, 1986.

L. De-moura and N. Bjørner, Z3: An Efficient SMT Solver, TACAS 2008, pp.337-340, 2008.
DOI : 10.1007/978-3-540-78800-3_24

T. Nipkow, Equational reasoning in Isabelle, Science of Computer Programming, vol.12, issue.2, pp.123-149, 1989.
DOI : 10.1016/0167-6423(89)90038-5

P. ?-ak and K. , The methods of improving and reorganizing natural deduction proofs, p.10, 2010.

P. ?-ak, K. , and K. , Methods of lemma extraction in natural deduction proofs Improving legibility of natural deduction proofs is not trivial, J. Autom. Reasoning Log. Meth. Comput. Sci, vol.50, issue.103, pp.217-228, 2013.

L. C. Paulson, Isabelle: A Generic Theorem Prover, LNCS, vol.828, 1994.
DOI : 10.1007/BFb0030541

L. C. Paulson, Strategic principles in the design of Isabelle, CADE-15 Workshop on Strategies in Automated Deduction, pp.11-17, 1998.

L. C. Paulson, A generic tableau prover and its integration with Isabelle, J. Univ. Comp. Sci, vol.5, pp.73-87, 1999.

L. C. Paulson, Three years of experience with Sledgehammer, a practical link between automated and interactive theorem provers, pp.1-10, 2010.

L. C. Paulson and J. C. Blanchette, Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers, EPiC EasyChair, vol.2, pp.1-11, 2010.

L. C. Paulson and K. W. Susanto, Source-Level Proof Reconstruction for Interactive Theorem Proving, TPHOLs 2007, pp.232-245, 2007.
DOI : 10.1007/978-3-540-74591-4_18

F. Pfenning, Analytic and non-analytic proofs, CADE-7, pp.393-413, 1984.
DOI : 10.1007/978-0-387-34768-4_23
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.150.3237

A. Reynolds, C. Tinelli, and L. De-moura, Finding conflicting instances of quantified formulas in SMT, 2014 Formal Methods in Computer-Aided Design (FMCAD), pp.195-202, 2014.
DOI : 10.1109/FMCAD.2014.6987613

A. Riazanov and A. Voronkov, The design and implementation of Vampire, AI Comm, vol.15, issue.2-3, pp.91-110, 2002.

A. J. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM, vol.12, issue.1, pp.23-41, 1965.
DOI : 10.1145/321250.321253

P. Rudnicki, Obvious inferences, Journal of Automated Reasoning, vol.3, issue.4, pp.383-393, 1987.
DOI : 10.1007/BF00247436

P. Rudnicki and J. Urban, Escape to ATP for Mizar, pp.46-59, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00677240

S. Schulz, System Description: E??1.8, LPAR-19, pp.735-743, 2013.
DOI : 10.1007/978-3-642-45221-5_49

S. J. Smolka, Robust, semi-intelligible Isabelle proofs from ATP proofs, 2013.

S. J. Smolka and J. C. Blanchette, Robust, semi-intelligible Isabelle proofs from ATP proofs, EasyChair, vol.14, pp.117-132, 2013.

A. Steckermeier, Extending Isabelle/HOL with the equality prover Waldmeister, 2014.

A. Stump, D. Oe, A. Reynolds, L. Hadarean, and C. Tinelli, SMT proof checking using a logical framework, Formal Methods in System Design, vol.7, issue.1, pp.91-118, 2013.
DOI : 10.1007/s10703-012-0163-3

N. Sultana and C. Benzmüller, Understanding LEO-II's proofs, IWIL 2012, EPiC, pp.33-52, 2013.

G. Sutcliffe, System Description: SystemOnTPTP, CADE-17, pp.406-410, 2000.
DOI : 10.1007/10721959_31

G. Sutcliffe, The TPTP Problem Library and Associated Infrastructure, Journal of Automated Reasoning, vol.13, issue.2, pp.337-362, 2009.
DOI : 10.1007/s10817-009-9143-8

G. Sutcliffe, The CADE-24 automated theorem proving system competition?CASC-24, AI Commun, vol.27, issue.4, pp.405-416, 2014.

G. Sutcliffe, J. Zimmer, and S. Schulz, TSTP data-exchange formats for automated theorem proving tools, Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems, pp.201-215, 2004.

R. Thiemann, Computing N-th roots using the Babylonian method Archive of Formal Proofs, 2013.

J. Urban, G. Sutcliffe, S. Trac, and Y. Puzis, Combining Mizar and TPTP semantic presentation and verification tools, Studies in Logic, Grammar and Rhetoric, pp.121-136, 2009.
DOI : 10.1007/11618027_23

M. Wampler-doty, A complete proof of the Robbins conjecture Archive of Formal Proofs, 2010.

T. Weber, Sat-based finite model generation for higher-order logic, 2008.

C. Weidenbach, D. Dimova, A. Fietzke, R. Kumar, M. Suda et al., SPASS Version 3.5, CADE-22, pp.140-145, 2009.
DOI : 10.1007/978-3-540-73595-3_38

M. Wenzel, Type classes and overloading in higher-order logic, LNCS, vol.1275, pp.307-322, 1997.
DOI : 10.1007/BFb0028402

M. Wenzel, Isabelle/Isar?A generic framework for human-readable proof documents, From Insight to Proof?Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar and Rhetoric, 2007.

J. Wickerson, M. Dodds, and M. J. Parkinson, Ribbon Proofs for Separation Logic, ESOP 2013, pp.189-208, 2013.
DOI : 10.1007/978-3-642-37036-6_12

J. Zimmer, A. Meier, G. Sutcliffe, and Y. Zhan, Integrated proof transformation services