. M. Bibliography, G. Armand, B. Faure, C. Grégoire, L. Keller 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 (CPP'11), pp.135-150, 2011.

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

[. Andreoli, R. Pareschi-andreoli, and R. Pareschi, Logic programming with sequent systems, a linear logic approach Linear ojects: Logical processes with built-in inheritance, Proc. of the Int. Work. on Extensions of Logic Programming Barendregt. Lambda calculi with types, pp.1-30445, 1989.

]. P. Bau00 and . Baumgartner, FDPLL -a first order Davis-Putnam-Longeman-Loveland procedure

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

F. Besson, P. Cornilleau, D. Pichardiebou97, ]. Baumgartner, C. Tinelli-]-p et al., Modular SMT proofs for fast reflexive checking inside Coq Certified Programs and Proofs Using reflection to build efficient and certified decision procedure s The model evolution calculus as a first-order DPLL method Model evolution with equality modulo built-in theories The duality of computation, TACS'97 Proc. of the 23rd Int. Conf. on Automated Deduction Proc. of the 5 th ACM SIGPLAN Int. Conf. on Functional Programming (ICFP'00), pp.151-166591, 1997.

]. V. Dan90 and . Danos, La logique linéaire appliquée à l'étude de divers processus de normalisation (et principalement du ?-calcul), Thèse de doctorat en mathématiques, p.20, 1990.

V. Danos, J. Joinet, and H. Schellinx, LKQ and LKT: sequent calculi for second order logic based upon dual linear decompositions of classical implication

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, 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

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

]. I. Gaz10 and . Gazeau, Private communication, p.99, 2010.

]. G. Gen35 and . Gentzen, Investigations into logical deduction, Gentzen collected works, pp.68-131, 1935.

]. Gir87, ]. R. Graham-lengrandjs97, R. Jr, and . Schrag, A new constructive logic: Classical logic Linear logic: its syntax and semantics Psyche: a proof-search engine based on sequent calculus with an LCF-style architecture Using csp look-back techniques to solve real-world sat instances, Linear logic. Theoret. Comput. Sci. Advances in Linear Logic Proc. of the 22nd Int. Conf. on Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux'13) AAAI/IAAI Thèse de doctoratLC09] S. Lescuyer and S. Conchon. Improving Coq propositional reasoning using a lazy CNF conversion scheme Proc. of the 7th Int. Conf. on Frontiers of combining systems (FroCoS'09), pp.1-101, 1987.

L. 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 9, 2011.
URL : https://hal.archives-ouvertes.fr/hal-01110478

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

O. Laurent, M. Quatrini, and L. T. De-falco, Polarized and focalized linear and classical proofs, Annals of Pure and Applied Logic, vol.134, issue.2-3, pp.217-264, 2005.
DOI : 10.1016/j.apal.2004.11.002
URL : https://hal.archives-ouvertes.fr/hal-00009133

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. 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

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

K. [. Silva, . Sakallahsta78-]-r, and . Statman, GRASP: a search algorithm for propositional satisfiability, Proc. of the 8th European Conf. on Logics in Artificial Intelligence, volume 2424 of LNAI, pp.506-521, 1978.
DOI : 10.1109/12.769433

T. Weber, SMT solvers: new oracles for the HOL theorem prover, International Journal on Software Tools for Technology Transfer, vol.7, issue.1, pp.419-429, 2011.
DOI : 10.1007/s10009-011-0188-8