. Acknowledgements, . Contributors, S. Of-psyche-include, A. Graham-lengrand, A. Mahboubi et al., References 1. J. M. Andreoli. Logic programming with focusing proofs in linear logic, J. Logic Comput, vol.2, issue.3, pp.297-347, 1992.

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

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

M. Farooque and S. Graham-lengrand, Sequent calculi with procedure calls, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00779199

M. Farooque, S. Graham-lengrand, and A. Mahboubi, A bisimulation between DPLL(T) and a proof-search strategy for the focused sequent calculus Available on Psyche's website, 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

M. Gordon, R. Milner, and C. Wadsworth, Edinburgh LCF: a mechanized logic of computation, LNCS, vol.78, 1979.
DOI : 10.1007/3-540-09724-4

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, J. C. Paulson, and . Blanchette, Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers, EPiC Series, vol.2, pp.1-11, 2010.

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