J. M. Andreoli, Logic Programming with Focusing Proofs in Linear Logic, Journal of Logic and Computation, vol.2, issue.3, pp.297-347, 1992.
DOI : 10.1093/logcom/2.3.297

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, Proc. of the 1st Int. Conf. on Certified Programs and Proofs, pp.135-150, 2011.
DOI : 10.1145/1217856.1217859

URL : https://hal.archives-ouvertes.fr/hal-00639130

C. Barrett, A. Stump, and C. Tinelli, The Satisfiability Modulo Theories Library

P. Baumgartner, FDPLL -a first order Davis-Putnam-Longeman- Loveland procedure, Proc. of the 17th Int. Conf. on Automated Deduction, pp.200-219, 2000.

P. Baumgartner and C. Tinelli, The model evolution calculus as a first-order DPLL method, Artificial Intelligence, vol.172, issue.4-5, pp.591-632, 2008.
DOI : 10.1016/j.artint.2007.09.005

P. Baumgartner and C. Tinelli, Model Evolution with Equality Modulo Built-in Theories, Proc. of the 23rd Int. Conf. on Automated Deduction, pp.85-100, 2011.
DOI : 10.1007/978-3-540-89439-1_20

P. Beame, H. Kautz, and A. Sabharwal, Towards understanding and harnessing the potential of clause learning, J. Artificial Intelligence Res, vol.22, pp.319-351, 2004.

F. Besson, P. Cornilleau, and D. Pichardie, Modular SMT Proofs for Fast Reflexive Checking Inside Coq, Certified Programs and Proofs, pp.151-166, 2011.
DOI : 10.1016/j.jal.2007.07.003

URL : https://hal.archives-ouvertes.fr/hal-00646960

J. C. Blanchette, S. Böhme, and L. C. Paulson, Extending Sledgehammer with SMT Solvers, Automated Deduction, pp.116-130, 2011.
DOI : 10.1007/BFb0028402

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

S. Boutin, Using reflection to build efficient and certified decision procedures, TACS'97, 1997.
DOI : 10.1007/BFb0014565

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

A. Charguéraud, Program verification through characteristic formulae, Proc. of the 15th ACM Intern. Conf. on Functional Programming, pp.321-332, 2010.

V. Danos, J. Joinet, and H. Schellinx, Abstract, The Journal of Symbolic Logic, vol.II, issue.03, pp.755-807, 1997.
DOI : 10.1007/BF00885763

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

M. Davis and H. Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM, vol.7, issue.3, pp.201-215, 1960.
DOI : 10.1145/321033.321034

M. Davis, G. Logemann, and D. W. Loveland, A machine program for theorem-proving, Communications of the ACM, vol.5, issue.7, pp.394-397, 1962.
DOI : 10.1145/368273.368557

N. Een and A. Biere, Effective preprocessing in SAT through variable and clause elimination, Proc. of the 8th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT'05), pp.61-75, 2005.

M. Farooque and S. Graham-lengrand, Sequent calculi with procedure calls Laboratoire d'informatique de l' ´ Ecole Polytechnique -CNRS, 2013.

J. Girard, Linear logic, Theoretical Computer Science, vol.50, issue.1, pp.1-101, 1987.
DOI : 10.1016/0304-3975(87)90045-4

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

J. Girard, A new constructive logic: classic logic, Mathematical Structures in Computer Science, vol.7, issue.2, pp.255-296, 1991.
DOI : 10.1016/0304-3975(87)90045-4

C. P. Gomes, B. Selman, and H. A. Kautz, Boosting combinatorial search through randomization, Proc. of the 15th National Conf. on Artificial Intelligence and 10th Innovative Applications of Artificial Intelligence Conf. (IAAI'98), pp.431-437, 1998.

S. Graham-lengrand, Psyche: A Proof-Search Engine Based on Sequent Calculus with an LCF-Style Architecture, Proc. of the 22nd Int. Conf. on Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux'13), 2013.
DOI : 10.1007/978-3-642-40537-2_14

URL : https://hal.archives-ouvertes.fr/hal-00906789

H. H. Hoos and T. Stützle, SATLIB: An online resource for research on SAT, SAT2000: Highlights of Satisfiability Research in the year, pp.283-292, 2000.

O. Laurent, Etude de la polarisation en logique, Thèse de doctorat, 2002.
URL : https://hal.archives-ouvertes.fr/tel-00007884

J. Leach, S. Nieva, and M. Rodríguez-artalejo, Constraint Logic Programming with Hereditary Harrop formulas, Theory and Practice of Logic Programming, vol.1, issue.04, pp.409-445, 2001.
DOI : 10.1017/S1471068401001041

S. Lengrand, R. Dyckhoff, and J. Mckinna, A focused sequent calculus framework for proof search in Pure Type Systems. Logic, Methods Comput. Science, vol.7, issue.1, 2011.
URL : https://hal.archives-ouvertes.fr/hal-01110478

S. Lescuyer and S. Conchon, Improving Coq propositional reasoning using a lazy CNF conversion scheme on Frontiers of combining systems (FroCoS'09), Proc. of the 7th Int. Conf, pp.287-303, 2009.

C. Liang and D. Miller, Focusing and polarization in linear, intuitionistic, and classical logics, Theoretical Computer Science, vol.410, issue.46, pp.4747-4768, 2009.
DOI : 10.1016/j.tcs.2009.07.041

D. Miller and V. Nigam, Incorporating Tables into Proofs, Proc. of the 16th Annual Conf. of the European Association for Computer Science Logic (CSL'07), pp.466-480
DOI : 10.1007/978-3-540-74915-8_35

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

D. Miller, G. Nadathur, F. Pfenning, and A. Scedrov, Uniform proofs as a foundation for logic programming, Annals of Pure and Applied Logic, vol.51, issue.1-2, pp.125-157, 1991.
DOI : 10.1016/0168-0072(91)90068-W

R. Milner, Lcf: A way of doing proofs with a machine, Proc. of the the 8th Int. Symp. on Mathematical Foundations of Computer Science, pp.146-159, 1979.
DOI : 10.1007/3-540-09526-8_11

M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik, Chaff, Proceedings of the 38th conference on Design automation , DAC '01, pp.530-535, 2001.
DOI : 10.1145/378239.379017

R. Nieuwenhuis, A. Oliveras, and C. Tinelli, Abstract DPLL and Abstract DPLL Modulo Theories, Proc. of the the 11th Int. Conf. on Logic for Programming Artificial Intelligence and Reasoning, pp.36-50, 2005.
DOI : 10.1007/978-3-540-32275-7_3

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

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. Tinelli and T. Weber, A DPLL-based calculus for ground satisfiability modulo theories SMT solvers: New oracles for the HOL theorem prover, Proc. of the 8th European Conf. on Logics in Artificial Intelligence, volume 2424 of LNAI, pp.308-319419, 2002.