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, vol.7086, pp.135-150, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00639130

M. Baaz, U. Egly, and A. Leitsch, Normal form transformations, Handbook of Automated Reasoning, vol.I, pp.273-333, 2001.

H. Barbosa, J. C. Blanchette, and P. Fontaine, Scalable fine-grained proofs for formula processing, CADE-26, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01590922

H. Barbosa, P. Fontaine, and A. Reynolds, Congruence closure with free variables, TACAS 2017, vol.10206, pp.214-230, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01590918

H. Barendregt and F. Wiedijk, The challenge of computer mathematics, Philosophical Transactions of the Royal Society of London-Series A, vol.363, pp.2351-2375, 1835.

C. Barrett, P. Fontaine, and C. Tinelli, The SMT-LIB standard: Version 2.5. Tech. rep., University of Iowa, 2015.

C. Barrett, L. De-moura, and P. Fontaine, Proofs in satisfiability modulo theories, Mathematical Logic and Foundations, vol.55, pp.23-44, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01095009

S. Berghofer and T. Nipkow, Proof terms for simply typed higher order logic, TPHOLs 2000, vol.1869, pp.38-52, 2000.

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, S. Böhme, M. Fleury, S. J. Smolka, and A. Steckermeier, Semi-intelligible Isar proofs from machine-generated proofs, J. Autom. Reasoning, vol.56, issue.2, pp.155-200, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01211748

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

S. Böhme, A. C. Fox, T. Sewell, and T. Weber, Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL, CPP 2011, vol.7086, pp.183-198, 2011.

S. Böhme and T. Weber, Fast LCF-style proof reconstruction for Z3, ITP 2010, vol.6172, pp.179-194, 2010.

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

G. Burel, A shallow embedding of resolution and superposition proofs into the ??-calculus modulo, EPiC Series in Computing, vol.14, pp.43-57, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00921513

D. Cousineau and G. Dowek, Embedding pure type systems in the lambda-Pi-calculus modulo, TLCA 2007, vol.4583, pp.102-117, 2007.

D. Déharbe, P. Fontaine, S. Merz, and B. Paleo, Exploiting symmetry in SMT problems, CADE-23, vol.6803, pp.222-236, 2011.

G. Ebner, S. Hetzl, G. Reis, M. Riener, S. Wolfsteiner et al., System description: GAPT 2.0, IJCAR 2016, vol.9706, pp.293-301, 2016.

B. Ekici, G. Katz, C. Keller, A. Mebsout, A. J. Reynolds et al., Extending SMTCoq, a certified checker for SMT (extended abstract), EPTCS, vol.210, pp.21-29, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01388984

P. Fontaine, J. Y. Marion, S. Merz, L. P. Nieto, and A. Tiu, Expressiveness + automation + soundness: Towards combining SMT solvers and interactive proof assistants, TACAS 2006, vol.3920, pp.167-181, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00001088

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

M. J. Gordon, R. Milner, and C. P. Wadsworth, Edinburgh LCF: A Mechanised Logic of Computation, vol.78, 1979.

S. Graham-lengrand, Psyche: A proof-search engine based on sequent calculus with an LCF-style architecture, TABLEAUX 2013, vol.8123, pp.149-156, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00906789

A. Guglielmi, A system of interaction and structure, ACM Trans. Comput. Log, vol.8, issue.1, p.1, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00441214

L. Hadarean, C. W. Barrett, A. Reynolds, C. Tinelli, and M. Deters, Fine grained SMT proofs for the theory of fixed-width bit-vectors, LPAR-20, vol.9450, pp.340-355, 2015.

R. Harper, F. Honsell, and G. D. Plotkin, A framework for defining logics, LICS '87, pp.194-204, 1987.

S. Hetzl, T. Libal, M. Riener, and M. Rukhaia, Understanding resolution proofs through Herbrand's theorem, Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), vol.8123, pp.157-171, 2013.

G. Katz, C. W. Barrett, C. Tinelli, A. Reynolds, and L. Hadarean, Lazy proofs for dpll(t)-based SMT solvers, pp.93-100, 2016.

E. Kotelnikov, L. Kov\'acs, M. Suda, and A. Voronkov, A clausal normal form translation for FOOL, GCAI 2016, vol.41, pp.53-71, 2016.

L. Kovács and A. Voronkov, First-order theorem proving and Vampire, CAV 2013, vol.8044, pp.1-35, 2013.

S. Mclaughlin, C. Barrett, and Y. Ge, Cooperating theorem provers: A case study combining HOL-Light and CVC Lite, Electr. Notes Theor. Comput. Sci, vol.144, issue.2, pp.43-51, 2006.

A. Meier, TRAMP: Transformation of machine-found proofs into natural deduction proofs at the assertion level (system description), CADE-17, vol.1831, pp.460-464, 2000.

D. Miller, Proof checking and logic programming, LOPSTR 2015, vol.9527, pp.3-17, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01390901

M. Moskal, Rocket-fast proof checking for SMT solvers, Tools and Algorithms for Construction and Analysis of Systems (TACAS), vol.4963, pp.486-500, 2008.

L. M. De-moura and N. Bjørner, Proofs and refutations, and Z3, LPAR 2008 Workshops, CEUR Workshop Proceedings, vol.418, 2008.

T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL: A Proof Assistant for Higher-Order Logic, vol.2283, 2002.

H. De-nivelle, Extraction of proofs from the clausal normal form transformation, CSL 2002, vol.2471, pp.584-598, 2002.

H. De-nivelle, Translation of resolution proofs into short first-order proofs without choice axioms, Inf. Comput, vol.199, issue.1-2, pp.24-54, 2005.

A. Nonnengart and C. Weidenbach, Computing small clause normal forms, Handbook of Automated Reasoning, vol.I, pp.335-367, 2001.

L. C. Paulson, A higher-order implementation of rewriting, Sci. Comput. Program, vol.3, issue.2, pp.119-149, 1983.

L. C. Paulson and K. W. Susanto, Source-level proof reconstruction for interactive theorem proving, TPHOLs 2007, vol.4732, pp.232-245, 2007.

G. Reger, M. Suda, and A. Voronkov, New techniques in clausal form generation, GCAI 2016, vol.41, pp.11-23, 2016.

S. Schulz, System description: E 1.8, vol.8312, pp.735-743, 2013.

A. Stump, Proof checking technology for satisfiability modulo theories, Electr. Notes Theor. Comput. Sci, vol.228, pp.121-133, 2009.

G. Sutcliffe, S. Schulz, K. Claessen, and P. Baumgartner, The TPTP typed first-order form with arithmetic, LPAR-18, vol.7180, pp.406-419, 2012.

G. Sutcliffe, J. Zimmer, and S. Schulz, Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems, Frontiers in Artificial Intelligence and Applications, vol.112, pp.201-215, 2004.

C. Weidenbach, D. Dimova, A. Fietzke, R. Kumar, M. Suda et al., SPASS version 3.5, vol.5663, pp.140-145, 2009.

J. Zimmer, A. Meier, G. Sutcliffe, and Y. Zhan, Integrated proof transformation services, WS, vol.7, 2004.