A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses, CPP 2011, pp.135-150, 2011. ,
DOI : 10.1145/1217856.1217859
URL : https://hal.archives-ouvertes.fr/hal-00639130
Congruence Closure with Free Variables, Tools and Algorithms for Construction and Analysis of Systems (TACAS), pp.214-230, 2017. ,
DOI : 10.1007/10721959_17
URL : https://hal.archives-ouvertes.fr/hal-01442691
The challenge of computer mathematics, Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences, vol.42, issue.1835, pp.2351-2375, 1835. ,
DOI : 10.1098/rsta.2005.1650
The SMT-LIB standard: Version 2.5. Tech. rep, 2015. ,
DOI : 10.1007/978-3-642-19583-9_2
Proof Terms for Simply Typed Higher Order Logic, TPHOLs 2000, pp.38-52, 2000. ,
DOI : 10.1007/3-540-44659-1_3
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.8649
A flexible proof format for SMT: A proposal, pp.15-26, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-00642544
Semi-intelligible Isar Proofs from Machine-Generated Proofs, Journal of Automated Reasoning, vol.27, issue.4, pp.155-200, 2016. ,
DOI : 10.1007/s10817-015-9335-3
URL : https://hal.archives-ouvertes.fr/hal-01211748
Reconstruction of Z3???s Bit-Vector Proofs in HOL4 and Isabelle/HOL, CPP 2011, pp.183-198, 2011. ,
DOI : 10.1016/j.jal.2007.07.003
Fast LCF-Style Proof Reconstruction for Z3, ITP 2010, pp.179-194, 2010. ,
DOI : 10.1007/978-3-642-14052-5_14
veriT: An Open, Trustable and Efficient SMT-Solver, CADE-22, pp.151-156, 2009. ,
DOI : 10.1007/978-3-540-73595-3_38
URL : https://hal.archives-ouvertes.fr/inria-00430634
A shallow embedding of resolution and superposition proofs into the ??-calculus modulo, EPiC Series in Computing EasyChair, vol.14, pp.43-57, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-01126321
Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo, TLCA 2007, pp.102-117, 2007. ,
DOI : 10.1007/978-3-540-73228-0_9
Exploiting Symmetry in SMT Problems, Proc. Conference on Automated Deduction (CADE), pp.222-236, 2011. ,
DOI : 10.1007/s00224-004-1192-0
System Description: GAPT 2.0, IJCAR 2016, pp.293-301, 2016. ,
DOI : 10.2307/2269949
Extending SMTCoq, a Certified Checker for SMT (Extended Abstract), HaTT 2016. EPTCS, pp.21-29, 2016. ,
DOI : 10.4204/EPTCS.210.5
URL : https://hal.archives-ouvertes.fr/hal-01388984
Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants, TACAS 2006, pp.167-181, 2006. ,
DOI : 10.1007/3-540-45620-1_26
URL : https://hal.archives-ouvertes.fr/inria-00001088
Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, 1993. ,
Psyche: A Proof-Search Engine Based on Sequent Calculus with an LCF-Style Architecture, TABLEAUX 2013, pp.149-156, 2013. ,
DOI : 10.1007/978-3-642-40537-2_14
URL : https://hal.archives-ouvertes.fr/hal-00906789
A system of interaction and structure, ACM Transactions on Computational Logic, vol.8, issue.1, p.1, 2007. ,
DOI : 10.1145/1182613.1182614
URL : https://hal.archives-ouvertes.fr/inria-00441214
Fine Grained SMT Proofs for the Theory of??Fixed-Width Bit-Vectors, LPAR-20, pp.340-355, 2015. ,
DOI : 10.1007/978-3-662-48899-7_24
A framework for defining logics, LICS '87, pp.194-204, 1987. ,
DOI : 10.1145/138027.138060
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.21.5854
Understanding resolution proofs through Herbrand's theorem Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), LNCS, vol.8123, pp.157-171, 2013. ,
Lazy proofs for DPLL(T)-based SMT solvers, 2016 Formal Methods in Computer-Aided Design (FMCAD), pp.93-100, 2016. ,
DOI : 10.1109/FMCAD.2016.7886666
First-Order Theorem Proving and Vampire, CAV 2013, pp.1-35, 2013. ,
DOI : 10.1007/978-3-642-39799-8_1
Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite, Electronic Notes in Theoretical Computer Science, vol.144, issue.2, pp.43-51, 2006. ,
DOI : 10.1016/j.entcs.2005.12.005
System Description: Tramp: Transformation of Machine-Found Proofs into Natural Deduction Proofs at the Assertion Level, CADE-17, pp.460-464, 2000. ,
DOI : 10.1007/10721959_37
Proof checking and logic programming, LOPSTR 2015, pp.3-17, 2015. ,
DOI : 10.1145/2790449.2790510
URL : https://hal.archives-ouvertes.fr/hal-01390901
Rocket-fast proof checking for SMT solvers Tools and Algorithms for Construction and Analysis of Systems, TACAS), pp.486-500, 2008. ,
Proofs and refutations, and Z3, LPAR 2008 Workshops. CEUR Workshop Proceedings, 2008. ,
Extraction of Proofs from the Clausal Normal Form Transformation, CSL 2002, pp.584-598, 2002. ,
DOI : 10.1007/3-540-45793-3_39
Translation of resolution proofs into short first-order proofs without choice axioms, Information and Computation, vol.199, issue.1-2, pp.24-54, 2005. ,
DOI : 10.1016/j.ic.2004.10.011
Computing Small Clause Normal Forms, Handbook of Automated Reasoning, pp.335-367, 2001. ,
DOI : 10.1016/B978-044450813-3/50008-4
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.42.222
A higher-order implementation of rewriting, Science of Computer Programming, vol.3, issue.2, pp.119-149, 1983. ,
DOI : 10.1016/0167-6423(83)90008-4
Source-Level Proof Reconstruction for Interactive Theorem Proving, TPHOLs 2007, pp.232-245, 2007. ,
DOI : 10.1007/978-3-540-74591-4_18
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.145.8845
System Description: E??1.8, LPAR-19, pp.735-743, 2013. ,
DOI : 10.1007/978-3-642-45221-5_49
Proof Checking Technology for Satisfiability Modulo Theories, Electronic Notes in Theoretical Computer Science, vol.228, pp.121-133, 2009. ,
DOI : 10.1016/j.entcs.2008.12.121
URL : http://doi.org/10.1016/j.entcs.2008.12.121
The TPTP Typed First-Order Form with Arithmetic, LPAR-18, pp.406-419, 2012. ,
DOI : 10.1007/978-3-642-28717-6_32
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.220.7526
TSTP data-exchange formats for automated theorem proving tools, Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems. Frontiers in Artificial Intelligence and Applications, pp.201-215, 2004. ,
SPASS Version 3.5, ) CADE-22, pp.140-145, 2009. ,
DOI : 10.1007/978-3-540-73595-3_38
Integrated proof transformation services, 2004. ,