A modular integration of SAT/ SMT solvers to Coq through proof witnesses, CPP 2011, vol.7086, pp.135-150, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-00639130
Normal form transformations, Handbook of Automated Reasoning, vol.I, pp.273-333, 2001. ,
Scalable fine-grained proofs for formula processing, CADE-26, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01590922
Congruence closure with free variables, TACAS 2017, vol.10206, pp.214-230, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01590918
The challenge of computer mathematics, Philosophical Transactions of the Royal Society of London-Series A, vol.363, pp.2351-2375, 1835. ,
, The SMT-LIB standard: Version 2.5. Tech. rep., University of Iowa, 2015.
Proofs in satisfiability modulo theories, Mathematical Logic and Foundations, vol.55, pp.23-44, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01095009
Proof terms for simply typed higher order logic, TPHOLs 2000, vol.1869, pp.38-52, 2000. ,
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, J. Autom. Reasoning, vol.56, issue.2, pp.155-200, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01211748
Proving theorems of higher-order logic with SMT solvers, 2012. ,
Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL, CPP 2011, vol.7086, pp.183-198, 2011. ,
Fast LCF-style proof reconstruction for Z3, ITP 2010, vol.6172, pp.179-194, 2010. ,
veriT: An open, trustable and efficient SMTsolver, LNCS, vol.5663, pp.151-156, 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00430634
A shallow embedding of resolution and superposition proofs into the ??-calculus modulo, EPiC Series in Computing, vol.14, pp.43-57, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00921513
Embedding pure type systems in the lambda-Pi-calculus modulo, TLCA 2007, vol.4583, pp.102-117, 2007. ,
Exploiting symmetry in SMT problems, CADE-23, vol.6803, pp.222-236, 2011. ,
System description: GAPT 2.0, IJCAR 2016, vol.9706, pp.293-301, 2016. ,
Extending SMTCoq, a certified checker for SMT (extended abstract), EPTCS, vol.210, pp.21-29, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01388984
Expressiveness + automation + soundness: Towards combining SMT solvers and interactive proof assistants, TACAS 2006, vol.3920, pp.167-181, 2006. ,
URL : https://hal.archives-ouvertes.fr/inria-00001088
Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, 1993. ,
, Edinburgh LCF: A Mechanised Logic of Computation, vol.78, 1979.
Psyche: A proof-search engine based on sequent calculus with an LCF-style architecture, TABLEAUX 2013, vol.8123, pp.149-156, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00906789
A system of interaction and structure, ACM Trans. Comput. Log, vol.8, issue.1, p.1, 2007. ,
URL : https://hal.archives-ouvertes.fr/inria-00441214
Fine grained SMT proofs for the theory of fixed-width bit-vectors, LPAR-20, vol.9450, pp.340-355, 2015. ,
A framework for defining logics, LICS '87, pp.194-204, 1987. ,
Understanding resolution proofs through Herbrand's theorem, Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), vol.8123, pp.157-171, 2013. ,
Lazy proofs for dpll(t)-based SMT solvers, pp.93-100, 2016. ,
A clausal normal form translation for FOOL, GCAI 2016, vol.41, pp.53-71, 2016. ,
First-order theorem proving and Vampire, CAV 2013, vol.8044, pp.1-35, 2013. ,
Cooperating theorem provers: A case study combining HOL-Light and CVC Lite, Electr. Notes Theor. Comput. Sci, vol.144, issue.2, pp.43-51, 2006. ,
TRAMP: Transformation of machine-found proofs into natural deduction proofs at the assertion level (system description), CADE-17, vol.1831, pp.460-464, 2000. ,
Proof checking and logic programming, LOPSTR 2015, vol.9527, pp.3-17, 2015. ,
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), vol.4963, pp.486-500, 2008. ,
Proofs and refutations, and Z3, LPAR 2008 Workshops, CEUR Workshop Proceedings, vol.418, 2008. ,
, Isabelle/HOL: A Proof Assistant for Higher-Order Logic, vol.2283, 2002.
Extraction of proofs from the clausal normal form transformation, CSL 2002, vol.2471, pp.584-598, 2002. ,
Translation of resolution proofs into short first-order proofs without choice axioms, Inf. Comput, vol.199, issue.1-2, pp.24-54, 2005. ,
Computing small clause normal forms, Handbook of Automated Reasoning, vol.I, pp.335-367, 2001. ,
A higher-order implementation of rewriting, Sci. Comput. Program, vol.3, issue.2, pp.119-149, 1983. ,
Source-level proof reconstruction for interactive theorem proving, TPHOLs 2007, vol.4732, pp.232-245, 2007. ,
New techniques in clausal form generation, GCAI 2016, vol.41, pp.11-23, 2016. ,
, System description: E 1.8, vol.8312, pp.735-743, 2013.
Proof checking technology for satisfiability modulo theories, Electr. Notes Theor. Comput. Sci, vol.228, pp.121-133, 2009. ,
The TPTP typed first-order form with arithmetic, LPAR-18, vol.7180, pp.406-419, 2012. ,
Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems, Frontiers in Artificial Intelligence and Applications, vol.112, pp.201-215, 2004. ,
, SPASS version 3.5, vol.5663, pp.140-145, 2009.
Integrated proof transformation services, WS, vol.7, 2004. ,