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, editors: 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ć, Tim King, Andrew Reynolds & Cesare Tinelli (2011): CVC4. In Ganesh Gopalakrishnan & Shaz Qadeer, editors: 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, editors: 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, editors: 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, editor: 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, editors: 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, editors: 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, editors: 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, editors: Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems, Frontiers in Artificial Intelligence and Applications 112, IOS Press, pp. 201-215.
