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. ,
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
Lambda calculi with types, Log. Comput. Sci, vol.2, issue.2 9, pp.117-309, 1992. ,
FDPLL -a first order Davis-Putnam-Longeman-Loveland procedure ,
Extending Sledgehammer with SMT Solvers, Automated Deduction, pp.116-130, 2011. ,
DOI : 10.1007/BFb0028402
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. ,
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. ,
LKQ and LKT: sequent calculi for second order logic based upon dual linear decompositions of classical implication ,
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
A machine program for theorem-proving, Communications of the ACM, vol.5, issue.7, pp.394-397, 1962. ,
DOI : 10.1145/368273.368557
A Computing Procedure for Quantification Theory, Journal of the ACM, vol.7, issue.3, pp.201-215, 1960. ,
DOI : 10.1145/321033.321034
Private communication, p.99, 2010. ,
Investigations into logical deduction, Gentzen collected works, pp.68-131, 1935. ,
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. ,
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
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
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
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
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
Solving SAT and SAT Modulo Theories, Journal of the ACM, vol.53, issue.6, pp.937-977, 2006. ,
DOI : 10.1145/1217856.1217859
GRASP: a search algorithm for propositional satisfiability, Proc. of the 8th European Conf. on Logics in Artificial Intelligence, pp.506-521, 1999. ,
DOI : 10.1109/12.769433
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