G. Armand, B. Faure, C. Grégoire, L. Keller, B. 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 (CPP'11), pp.135-150, 2011.
DOI : 10.1145/1217856.1217859
URL : https://hal.archives-ouvertes.fr/hal-00639130

]. J. And92 and . Andreoli, Logic programming with focusing proofs in linear logic, J. Logic Comput, vol.2, issue.3, pp.297-347, 1992.

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

[. Barrett, R. Nieuwenhuis, A. Oliveras, and C. Tinelli, Splitting on Demand in SAT Modulo Theories, Proc. of the the 13th Int. Conf. on Logic for Programming Artificial Intelligence and Reasoning (LPAR'06), pp.512-526, 2006.
DOI : 10.1007/11916277_35

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, Nikolaj Bjørner and Viorica Sofronie- Stokkermans Proc. of the 23rd Int. Conf. on Automated Deduction, pp.85-100, 2011.
DOI : 10.1007/978-3-540-89439-1_20

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

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

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

[. Laurent, Polarized proof-nets and lambda-mu calculus, Theoret . Comput. Sci, vol.1, issue.290, pp.161-188, 2003.
DOI : 10.1016/s0304-3975(01)00297-3
URL : https://hal.archives-ouvertes.fr/hal-00009114

[. 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.287-303, 2009.
DOI : 10.1016/j.jal.2007.07.003

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, 2007.
DOI : 10.1007/978-3-540-74915-8_35

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

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

[. 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, A DPLL-Based Calculus for Ground Satisfiability Modulo Theories, Proc. of the 8th European Conf. on Logics in Artificial Intelligence, volume 2424 of LNAI, pp.308-319, 2002.
DOI : 10.1007/3-540-45757-7_26