M. Armand, B. Grégoire, A. Spiwack, and L. Théry, Extending Coq with Imperative Features and Its Application to SAT Verification, pp.83-98
DOI : 10.1007/978-3-642-14052-5_8

URL : https://hal.archives-ouvertes.fr/inria-00502496

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

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

S. Böhme and T. Weber, Fast LCF-Style Proof Reconstruction for Z3, pp.179-194
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-156, 2009.
DOI : 10.1007/978-3-540-73595-3_38

URL : https://hal.archives-ouvertes.fr/inria-00430634

R. E. Bryant, Symbolic Boolean manipulation with ordered binary-decision diagrams, ACM Computing Surveys, vol.24, issue.3, pp.293-318, 1992.
DOI : 10.1145/136035.136043

URL : http://akebono.stanford.edu/users/nanni/courses/EE318/bryant92.pdf

A. Stephen and . Cook, A Short Proof of the Pigeon Hole Principle using Extended Resolution, ACM SIGACT News, vol.8, issue.4, pp.28-32, 1976.

A. Stephen, R. A. Cook, and . Reckhow, On the Lengths of Proofs in the Propositional Calculus (Preliminary Version), STOC, pp.135-148, 1974.

D. Marcello, . Agostino, M. Dov, R. Gabbay, J. Hähnle et al., Handbook of Tableau Methods, 1999.

D. Deharbe, P. Fontaine, and B. W. Paleo, Quantier Inference Rules for SMT proofs, PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, pp.33-39, 2011.

R. Drechsler, J. Shi, and G. Fey, Synthesis of Fully Testable Circuits From BDDs, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol.23, issue.3, pp.440-443, 2004.
DOI : 10.1109/TCAD.2004.823342

N. Eén and N. Sörensson, An Extensible SAT-solver, Lecture Notes in Computer Science, vol.2919, pp.502-518, 2003.
DOI : 10.1007/978-3-540-24605-3_37

G. Fey, J. Shi, and R. Drechsler, BDD circuit optimization for path delay fault testability, Euromicro Symposium on Digital System Design, 2004. DSD 2004., pp.168-172, 2004.
DOI : 10.1109/DSD.2004.1333273

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.12.2296

Z. Fu, Y. Marhajan, S. Malik, and . Zchaff, Research Web Page, 2007.

A. Van-gelder, Verifying RUP Proofs of Propositional Unsatisfiability, In ISAIM, 2008.

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

D. Kroening and O. Strichman, Decision Procedures: an Algorithmic Point of View, 2008.
DOI : 10.1007/978-3-662-50497-0

A. Layeb, N. Tabib, and B. Brirem, Genetic Algorithm and Variable Neighbourhood Search for BDD Variable Ordering Problem, INFOCOMP Journal of Computer Science, vol.10, issue.1, pp.29-35, 2011.

R. Nieuwenhuis, A. Oliveras, and C. Tinelli, Solving SAT and SAT Modulo Theories, Journal of the ACM, vol.53, issue.6, pp.937-977, 2006.
DOI : 10.1145/1217856.1217859

C. Lawrence and . Paulson, A Generic Tableau Prover and its Integration with Isabelle, J. UCS, vol.5, issue.3, pp.73-87, 1999.

C. Lawrence, J. C. Paulson, and . Blanchette, Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers, International Workshop on the Implementation of Logics (IWIL-2010), 2010.

L. C. Paulson, Isabelle -A Generic Theorem Prover (with a contribution by, Lecture Notes in Computer Science, vol.828, 1994.

N. Peltier, Extended resolution simulates binary decision diagrams, Discrete Applied Mathematics, vol.156, issue.6, pp.825-837, 2008.
DOI : 10.1016/j.dam.2006.11.012

URL : http://doi.org/10.1016/j.dam.2006.11.012

C. Sinz and A. Biere, Extended Resolution Proofs for Conjoining BDDs, Lecture Notes in Computer Science, vol.3967, pp.600-611, 2006.
DOI : 10.1007/11753728_60

R. M. Smullyan, First-Order Logic, 1968.
DOI : 10.1201/b10689-23

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

A. Urquhart, Abstract, Bulletin of Symbolic Logic, vol.35, issue.04, pp.425-467, 1995.
DOI : 10.1145/136035.136043