C. Barret, A. Stump, and C. Tinelli, The SMT-LIB standard: Version 2.0, 2010, Latest official release of Version 2.0 of the SMT-LIB standard

S. Böhme and T. Weber, Fast LCF-Style Proof Reconstruction for Z3, ITP'2010, pp.179-194, 2010.
DOI : 10.1007/978-3-642-14052-5_14

T. Bouton, D. C. De-oliveira, D. Déharbe, and P. Fontaine, veriT: an open, trustable and efficient SMTsolver, CADE'09, pp.151-156, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00430634

L. M. De-moura and N. Bjørner, Proofs and Refutations, and Z3, Proc. of the LPAR 2008 Workshops, volume 418 of CEUR Workshop Proceedings, 2008.

L. M. De-moura and N. Bjørner, Z3: An Efficient SMT Solver, TACAS'08, pp.337-340, 2008.
DOI : 10.1007/978-3-540-78800-3_24

D. Déharbe, P. Fontaine, and B. , Quantifier inference rules for SMT proofs, Workshop on Proof eXchange for Theorem Proving (PxTP), 2011.

S. Mclaughlin, C. Barrett, and Y. Ge, Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite, PDPAR '05, pp.43-51, 2006.
DOI : 10.1016/j.entcs.2005.12.005

A. Stump and D. L. Dill, Faster Proof Checking in the Edinburgh Logical Framework, CADE-18, pp.392-407, 2002.
DOI : 10.1007/3-540-45620-1_32

G. Sutcliffe, J. Zimmer, and S. Schulz, TSTP Data-Exchange Formats for Automated Theorem Proving Tools, Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems, pp.201-215, 2004.