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

H. Barbosa, P. Fontaine, and A. Reynolds, Congruence Closure with Free Variables, TACAS 2017, pp.214-230, 2017.
DOI : 10.1007/10721959_17
URL : https://hal.archives-ouvertes.fr/hal-01442691

C. Barrett, P. Fontaine, and C. Tinelli, The SMT-LIB standard: Version 2.5. Tech. rep, 2015.
DOI : 10.1007/978-3-642-19583-9_2

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, Journal of Automated Reasoning, vol.27, issue.4, pp.155-200, 2016.
DOI : 10.1007/978-3-642-37036-6_12
URL : https://hal.archives-ouvertes.fr/hal-01211748

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 SMT-Solver, CADE-22, pp.151-156, 2009.
DOI : 10.1007/978-3-540-73595-3_38
URL : https://hal.archives-ouvertes.fr/inria-00430634

D. Déharbe, P. Fontaine, S. Merz, and B. W. Paleo, Exploiting Symmetry in SMT Problems, CADE-23, pp.222-236, 2011.
DOI : 10.1007/s00224-004-1192-0

G. Ebner, S. Hetzl, G. Reis, M. Riener, S. Wolfsteiner et al., System Description: GAPT 2.0, IJCAR 2016, pp.293-301, 2016.
DOI : 10.1007/11814771_7

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, pp.340-355, 2015.
DOI : 10.1007/978-3-662-48899-7_24

R. Harper, F. Honsell, and G. D. Plotkin, A framework for defining logics, LICS '87, pp.194-204, 1987.
DOI : 10.1145/138027.138060
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.21.5854

G. Katz, C. W. Barrett, C. Tinelli, A. Reynolds, and L. Hadarean, Lazy proofs for DPLL(T)-based SMT solvers, 2016 Formal Methods in Computer-Aided Design (FMCAD), pp.93-100, 2016.
DOI : 10.1109/FMCAD.2016.7886666

L. Kovács and A. Voronkov, First-Order Theorem Proving and Vampire, CAV 2013, pp.1-35, 2013.
DOI : 10.1007/978-3-642-39799-8_1

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

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

H. De-nivelle, Translation of resolution proofs into short first-order proofs without choice axioms, Information and Computation, vol.199, issue.1-2, pp.24-54, 2005.
DOI : 10.1016/j.ic.2004.10.011

A. Nonnengart and C. Weidenbach, Computing Small Clause Normal Forms, Handbook of Automated Reasoning, pp.335-367, 2001.
DOI : 10.1016/B978-044450813-3/50008-4
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.42.222

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
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.145.8845

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

A. Stump, Proof Checking Technology for Satisfiability Modulo Theories, Electronic Notes in Theoretical Computer Science, vol.228, pp.121-133, 2009.
DOI : 10.1016/j.entcs.2008.12.121
URL : http://doi.org/10.1016/j.entcs.2008.12.121

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. Frontiers in Artificial Intelligence and Applications, pp.201-215, 2004.

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