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

B. Barras, S. Boutin, C. Cornes, J. Courant, J. C. Filliâtre et al., The Coq proof assistant: reference manual, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00069968

C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanovi´cjovanovi´c et al., CVC4, Computer Aided Verification -23rd International Conference, CAV 2011, pp.171-177, 2011.
DOI : 10.1007/3-540-45657-0_40

C. Barrett, A. Stump, and &. Tinelli, The SMT-LIB Standard: Version 2.0, Proceedings of the 8th International Workshop on Satisfiability Modulo Theories, 2010.

F. Besson, Fast Reflexive Arithmetic Tactics the Linear Case and Beyond, TYPES, Lecture Notes in Computer Science 4502, pp.48-62, 2006.
DOI : 10.1007/978-3-540-74464-1_4

F. Besson, P. Fontaine, and &. L. Théry, A Flexible Proof Format for SMT: a Proposal, PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, pp.15-26, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00642544

J. Christian-blanchette, C. Kaliszyk, L. C. Paulson, and &. Urban, Hammering towards QED, J. Formalized Reasoning, vol.9, issue.1, pp.101-148, 2016.

S. Böhme, C. J. Anthony, T. Fox, &. Sewell, and . Weber, Reconstruction of Z3???s Bit-Vector Proofs in HOL4 and Isabelle/HOL, pp.183-198, 2011.
DOI : 10.1016/j.jal.2007.07.003

S. Böhme and &. Weber, Fast LCF-Style Proof Reconstruction for Z3, Interactive Theorem Proving, First International Conference, pp.179-19410, 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, Lecture Notes in Computer Science, vol.144, issue.2, pp.151-15610, 2009.
DOI : 10.1007/978-3-540-73595-3_38
URL : https://hal.archives-ouvertes.fr/inria-00430634

A. Van-gelder, Producing and verifying extremely large propositional refutations, Annals of Mathematics and Artificial Intelligence, vol.43, issue.1???4, pp.329-372, 2012.
DOI : 10.1007/s10472-012-9322-x

G. Gonthier and &. Mahboubi, An introduction to small scale reflection in Coq, J. Formalized Reasoning, vol.3, issue.2, pp.95-15210, 1979.
URL : https://hal.archives-ouvertes.fr/inria-00515548

L. Hadarean, C. W. Barrett, and A. Reynolds, Cesare Tinelli & Morgan Deters (2015): Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors

R. Harper, F. Honsell, &. Gordon, and D. Plotkin, A framework for defining logics, Journal of the ACM, vol.40, issue.1, pp.143-184, 1993.
DOI : 10.1145/138027.138060

M. Heule, W. A. Hunt-jr, and . Nathan-wetzler, Verifying Refutations with Extended Resolution, 24th International Conference on Automated Deduction, Lake Placid, pp.345-35910, 2013.
DOI : 10.1007/978-3-642-38574-2_24

O. Kullmann, On a generalization of extended resolution, Discrete Applied Mathematics, vol.96, issue.97, pp.96-97, 1999.
DOI : 10.1016/S0166-218X(99)00037-2

P. Letouzey, A New Extraction for Coq, Types for Proofs and Programs, pp.200-21910, 2002.
DOI : 10.1007/3-540-39185-1_12
URL : https://hal.archives-ouvertes.fr/hal-00150914

S. Yogesh, Z. Mahajan, &. Fu, and . Malik, Zchaff2004: An Efficient SAT Solver, Theory and Applications of Satisfiability Testing, 7th International Conference, pp.360-37510, 2004.

C. Lawrence, &. Paulson, and . Blanchette, Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers, The 8th International Workshop on the Implementation of Logics, IWIL 2010, pp.1-11, 2010.

A. Stump, D. Oe, A. Reynolds, L. Hadarean, and &. 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

G. Tseitin, On the Complexity of Proofs in Propositional Logics, In: Seminars in Mathematics, vol.8, pp.466-483, 1970.

T. Weber, SAT-based Finite Model Generation for Higher-Order Logic, 2008.

N. Wetzler, M. Heule, &. Warren, and A. Hunt-jr, Mechanical Verification of SAT Refutations with Extended Resolution, Interactive Theorem Proving -4th International Conference, ITP 2013, pp.229-24410, 2013.
DOI : 10.1007/978-3-642-39634-2_18