Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry & Benjamin Werner (2011):
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses.
In: Jean-Pierre Jouannaud & Zhong Shao: CPP 2011,
LNCS 7086.
Springer,
pp. 135–150,
doi:10.1007/978-3-642-25379-9_12.
Haniel Barbosa, Jasmin C. Blanchette, Mathias Fleury & Pascal Fontaine (2019):
Scalable Fine-Grained Proofs for Formula Processing.
Journal of Automated Reasoning,
doi:10.1007/s10817-018-09502-y.
Haniel Barbosa, Jasmin C. Blanchette, Mathias Fleury, Pascal Fontaine & Hans-Jörg Schurr (2019):
Better SMT proofs for easier reconstruction.
In: Thomas C. Hales, Cezary Kaliszyk, Ramana Kumar, Stephan Schulz & Josef Urban: AITP 2019.
Clark Barrett, Pascal Fontaine & Cesare Tinelli (2016):
The Satisfiability Modulo Theories Library (SMT-LIB).
www.SMT-LIB.org.
Clark Barrett, Roberto Sebastiani, Sanjit Seshia & Cesare Tinelli (2009):
Satisfiability Modulo Theories.
In: Armin Biere, Marijn J. H. Heule, Hans van Maaren & Toby Walsh: Handbook of Satisfiability, chapter 26,
Frontiers in Artificial Intelligence and Applications 185.
IOS Press,
pp. 825–885.
Frédéric Besson, Pascal Fontaine & Laurent Théry (2011):
A Flexible Proof Format for SMT: A Proposal.
In: Pascal Fontaine & Aaron Stump: PxTP 2011,
pp. 15–26.
Available at https://hal.inria.fr/hal-00642544/.
Jasmin C. Blanchette, Sascha Böhme, Mathias Fleury, Steffen J. Smolka & Albert Steckermeier (2016):
Semi-intelligible Isar Proofs from Machine-Generated Proofs.
Journal of Automated Reasoning 56(2),
pp. 155–200,
doi:10.1007/s10817-015-9335-3.
Sascha Böhme & Tjark Weber (2010):
Fast LCF-Style Proof Reconstruction for Z3.
In: Matt Kaufmann & Lawrence C. Paulson: ITP 2010,
LNCS 6172.
Springer,
pp. 179–194,
doi:10.1007/978-3-642-14052-5_14.
Thomas Bouton, Diego C. B. de Oliveira, David Déharbe & Pascal Fontaine (2009):
veriT: An Open, Trustable and Efficient SMT-solver.
In: Renate A. Schmidt: CADE 2009,
LNCS 5663.
Springer,
pp. 151–156,
doi:10.1007/978-3-642-02959-2_12.
Sebastian Buchwald, Denis Lohner & Sebastian Ullrich (2016):
Verified construction of static single assignment form.
In: CC.
ACM,
pp. 67–76,
doi:10.1145/2892208.2892211.
David Déharbe, Pascal Fontaine & Bruno Woltzenlogel Paleo (2011):
Quantifier Inference Rules for SMT Proofs.
In: Pascal Fontaine & Aaron Stump: PxTP 2011,
pp. 33–39.
Available at https://hal.inria.fr/hal-00642535.
Burak Ekici, Guy Katz, Chantal Keller, Alain Mebsout, Andrew J. Reynolds & Cesare Tinelli (2016):
Extending SMTCoq, a Certified Checker for SMT (Extended Abstract).
In: Jasmin C. Blanchette & Cezary Kaliszyk: HaTT 2016,
EPTCS 210,
pp. 21–29,
doi:10.4204/EPTCS.210.5.
Sean McLaughlin, Clark Barrett & Yeting Ge (2006):
Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite.
Electronic Notes in Theoretical Computer Science 144(2),
pp. 43–51,
doi:10.1016/j.entcs.2005.12.005.
Leonardo de Moura & Nikolaj Bjørner (2008):
Z3: An Efficient SMT Solver.
In: C. R. Ramakrishnan & Jakob Rehof: TACAS 2008,
LNCS 4963.
Springer,
pp. 337–340,
doi:10.1007/978-3-540-78800-3_24.
Anders Schlichtkrull, Jasmin C. Blanchette, Dmitriy Traytel & Uwe Waldmann (2018):
Formalization of Bachmair and Ganzinger's Ordered Resolution Prover.
Archive of Formal Proofs.
http://isa-afp.org/entries/Ordered_Resolution_Prover.html, Formal proof development.
Anders Schlichtkrull, Jasmin C. Blanchette, Dmitriy Traytel & Uwe Waldmann (2018):
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover.
In: IJCAR,
LNCS 10900.
Springer,
pp. 89–107,
doi:10.1007/978-3-319-94205-6_7.
Alexander Schrijver (1999):
Theory of Linear and Integer Programming.
Wiley - Interscience Series in Discrete Mathematics and Optimization.
Wiley.
Aaron Stump, Duckki Oe, Andrew Reynolds, Liana Hadarean & Cesare Tinelli (2013):
SMT Proof Checking Using a Logical Framework.
Formal Methods in System Design 42(1),
pp. 91–118,
doi:10.1007/s10703-012-0163-3.
Sebastian Ullrich & Denis Lohner (2016):
Verified Construction of Static Single Assignment Form.
Archive of Formal Proofs.
http://isa-afp.org/entries/Formal_SSA.html, Formal proof development.
eptcs@eptcs.org