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: Certified Programs and Proofs,
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.
Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovi\'c, Tim King, Andrew Reynolds & Cesare Tinelli (2011):
CVC4.
In: Ganesh Gopalakrishnan & Shaz Qadeer: Computer Aided Verification (CAV).
Springer,
pp. 171–177,
doi:10.1007/978-3-642-22110-1_14.
Clark Barrett, Leonardo De Moura & Pascal Fontaine (2015):
Proofs in satisfiability modulo theories.
All about proofs, Proofs for all 55(1),
pp. 23–44.
Clark Barrett, Pascal Fontaine & Cesare Tinelli (2017):
The SMT-LIB Standard: Version 2.6.
Technical Report.
Department of Computer Science, The University of Iowa.
Available at www.SMT-LIB.org.
Clark W. Barrett & Cesare Tinelli (2018):
Satisfiability Modulo Theories.
In: Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith & Roderick Bloem: Handbook of Model Checking..
Springer,
pp. 305–343,
doi:10.1007/978-3-319-10575-8_11.
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.
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 22,
LNCS 5663.
Springer Berlin Heidelberg,
pp. 151–156,
doi:10.1007/978-3-642-02959-2_12.
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.
Peter J. Downey, Ravi Sethi & Robert Endre Tarjan (1980):
Variations on the Common Subexpression Problem.
J. ACM 27(4),
pp. 758–771,
doi:10.1145/322217.322228.
Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds & Clark Barrett (2017):
SMTCoq: A Plug-In for Integrating SMT Solvers into Coq.
In: Rupak Majumdar & Viktor Kunčak: CAV 2017,
LNCS 10426.
Springer,
pp. 126–133,
doi:10.1007/978-3-319-63390-9_7.
Mathias Fleury & Hans-Jörg Schurr (2019):
Reconstructing veriT Proofs in Isabelle/HOL.
In: Giselle Reis & Haniel Barbosa: PxTP 2019,
EPTCS 301,
pp. 36–50,
doi:10.4204/EPTCS.301.6.
Greg Nelson & Derek C. Oppen (1980):
Fast Decision Procedures Based on Congruence Closure.
J. ACM 27(2),
pp. 356–364,
doi:10.1145/322186.322198.
Hans-Jörg Schurr, Mathias Fleury & Martin Desharnais (2021):
Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant.
In: CADE 28,
LNCS.
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.
Geoff Sutcliffe, Jürgen Zimmer & Stephan Schulz (2004):
TSTP Data-Exchange Formats for Automated Theorem Proving Tools.
In: Weixiong Zhang & Volker Sorge: Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems,
Frontiers in Artificial Intelligence and Applications 112.
IOS Press,
pp. 201–215.
eptcs@eptcs.org