@inproceedings(DBLP:conf/cpp/ArmandFGKTW11,
 author       = {Micha{\"e}l Armand and Germain Faure and Benjamin Gr{\'e}goire and Chantal Keller and Laurent Th{\'e}ry and Benjamin Werner},
 year         = {2011},
 title        = {{A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses}},
 editor       = {Jouannaud and Shao},
 pages        = {135--150},
 doi          = {10.1007/978-3-642-25379-9\_12},
)
@techreport(barras:cpa,
 author       = {B.~Barras and S.~Boutin and C.~Cornes and J.~Courant and J.C. Filli\^atre and E.~Gimenez and H.~Herbelin and G.~Huet and C.~Mu\~noz and C.~Murthy},
 year         = {2000},
 title        = {{The Coq proof assistant: reference manual}},
 type         = {Technical Report},
 institution  = {INRIA},
)
@inproceedings(DBLP:conf/cav/BarrettCDHJKRT11,
 author       = {Clark Barrett and Christopher~L. Conway and Morgan Deters and Liana Hadarean and Dejan Jovanovi\'c and Tim King and Andrew Reynolds and Cesare Tinelli},
 year         = {2011},
 title        = {{CVC4}},
 editor       = {Ganesh Gopalakrishnan and Shaz Qadeer},
 booktitle    = {Computer Aided Verification - 23rd International Conference, {CAV} 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {6806},
 publisher    = {Springer},
 pages        = {171--177},
 doi          = {10.1007/978-3-642-22110-1\_14},
)
@inproceedings(BarST-SMT-10,
 author       = {Clark Barrett and Aaron Stump and Cesare Tinelli},
 year         = {2010},
 title        = {{The SMT-LIB Standard: Version 2.0}},
 editor       = {A.~Gupta and D.~Kroening},
 booktitle    = {Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK)},
)
@inproceedings(DBLP:conf/types/Besson06,
 author       = {F.~Besson},
 year         = {2006},
 title        = {{Fast Reflexive Arithmetic Tactics the Linear Case and Beyond}},
 editor       = {Thorsten Altenkirch and Conor McBride},
 booktitle    = {TYPES},
 series       = {Lecture Notes in Computer Science},
 volume       = {4502},
 publisher    = {Springer},
 pages        = {48--62},
 doi          = {10.1007/978-3-540-74464-1\_4},
)
@inproceedings(BessonFT11,
 author       = {F.~Besson and P.~Fontaine and L.~Th{\'e}ry},
 year         = {2011},
 title        = {{A Flexible Proof Format for SMT: a Proposal}},
 booktitle    = {PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving August 1, 2011 Affiliated with CADE 2011, 31 July-5 August 2011 Wroc{\l}aw, Poland},
 pages        = {15--26},
)
@article(DBLP:journals/jfrea/BlanchetteKPU16,
 author       = {Jasmin~Christian Blanchette and Cezary Kaliszyk and Lawrence~C. Paulson and Josef Urban},
 year         = {2016},
 title        = {Hammering towards {QED}},
 journal      = {J. Formalized Reasoning},
 volume       = {9},
 number       = {1},
 pages        = {101--148},
 doi          = {10.6092/issn.1972-5787/4593},
)
@inproceedings(DBLP:conf/cpp/BohmeFSW11,
 author       = {Sascha B{\"{o}}hme and Anthony C.~J. Fox and Thomas Sewell and Tjark Weber},
 year         = {2011},
 title        = {Reconstruction of Z3's Bit-Vector Proofs in {HOL4} and Isabelle/HOL},
 editor       = {Jouannaud and Shao},
 pages        = {183--198},
 doi          = {10.1007/978-3-642-25379-9\_15},
)
@inproceedings(DBLP:conf/itp/BohmeW10,
 author       = {Sascha B{\"{o}}hme and Tjark Weber},
 year         = {2010},
 title        = {Fast LCF-Style Proof Reconstruction for {Z3}},
 editor       = {Matt Kaufmann and Lawrence~C. Paulson},
 booktitle    = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {6172},
 publisher    = {Springer},
 pages        = {179--194},
 doi          = {10.1007/978-3-642-14052-5\_14},
)
@inproceedings(DBLP:conf/cade/BoutonODF09,
 author       = {T.~Bouton and D.C.B. de~Oliveira and D.~D{\'e}harbe and P.~Fontaine},
 year         = {2009},
 title        = {{veriT: An Open, Trustable and Efficient SMT-Solver}},
 editor       = {R.~A. Schmidt},
 booktitle    = {CADE},
 series       = {Lecture Notes in Computer Science},
 volume       = {5663},
 publisher    = {Springer},
 pages        = {151--156},
 doi          = {10.1007/978-3-642-02959-2\_12},
)
@article(DBLP:journals/amai/Gelder12,
 author       = {Allen~Van Gelder},
 year         = {2012},
 title        = {{Producing and verifying extremely large propositional refutations - Have your cake and eat it too}},
 journal      = {Ann. Math. Artif. Intell.},
 volume       = {65},
 number       = {4},
 pages        = {329--372},
 doi          = {10.1007/s10472-012-9322-x},
)
@article(DBLP:journals/jfrea/GonthierM10,
 author       = {Georges Gonthier and Assia Mahboubi},
 year         = {2010},
 title        = {An introduction to small scale reflection in Coq},
 journal      = {J. Formalized Reasoning},
 volume       = {3},
 number       = {2},
 pages        = {95--152},
 doi          = {10.6092/issn.1972-5787/1979},
)
@inproceedings(DBLP:conf/lpar/HadareanBRTD15,
 author       = {Liana Hadarean and Clark~W. Barrett and Andrew Reynolds and Cesare Tinelli and Morgan Deters},
 year         = {2015},
 title        = {{Fine Grained {SMT} Proofs for the Theory of Fixed-Width Bit-Vectors}},
 editor       = {Martin Davis and Ansgar Fehnker and Annabelle McIver and Andrei Voronkov},
 booktitle    = {Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, {LPAR-20} 2015, Suva, Fiji, November 24-28, 2015, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {9450},
 publisher    = {Springer},
 pages        = {340--355},
 doi          = {10.1007/978-3-662-48899-7\_24},
)
@article(DBLP:journals/jacm/HarperHP93,
 author       = {Robert Harper and Furio Honsell and Gordon~D. Plotkin},
 year         = {1993},
 title        = {A Framework for Defining Logics},
 journal      = {J. {ACM}},
 volume       = {40},
 number       = {1},
 pages        = {143--184},
 doi          = {10.1145/138027.138060},
)
@inproceedings(DBLP:conf/cade/HeuleHW13,
 author       = {Marijn Heule and Warren A.~Hunt Jr. and Nathan Wetzler},
 year         = {2013},
 title        = {Verifying Refutations with Extended Resolution},
 editor       = {Maria~Paola Bonacina},
 booktitle    = {Automated Deduction - {CADE-24} - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {7898},
 publisher    = {Springer},
 pages        = {345--359},
 doi          = {10.1007/978-3-642-38574-2\_24},
)
@proceedings(DBLP:conf/cpp/2011,
 editor       = {Jean-Pierre Jouannaud and Zhong Shao},
 year         = {2011},
 title        = {Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {7086},
 publisher    = {Springer},
 doi          = {10.1007/978-3-642-25379-9},
)
@article(DBLP:journals/dam/Kullmann99,
 author       = {Oliver Kullmann},
 year         = {1999},
 title        = {On a Generalization of Extended Resolution},
 journal      = {Discrete Applied Mathematics},
 volume       = {96-97},
 pages        = {149--176},
 doi          = {10.1016/S0166-218X(99)00037-2},
)
@inproceedings(DBLP:conf/types/Letouzey02,
 author       = {Pierre Letouzey},
 year         = {2002},
 title        = {{A New Extraction for Coq}},
 editor       = {Herman Geuvers and Freek Wiedijk},
 booktitle    = {Types for Proofs and Programs, Second International Workshop, {TYPES} 2002, Berg en Dal, The Netherlands, April 24-28, 2002, Selected Papers},
 series       = {Lecture Notes in Computer Science},
 volume       = {2646},
 publisher    = {Springer},
 pages        = {200--219},
 doi          = {10.1007/3-540-39185-1\_12},
)
@inproceedings(DBLP:conf/sat/MahajanFM04,
 author       = {Yogesh~S. Mahajan and Zhaohui Fu and Sharad Malik},
 year         = {2004},
 title        = {Zchaff2004: An Efficient {SAT} Solver},
 editor       = {Holger~H. Hoos and David~G. Mitchell},
 booktitle    = {Theory and Applications of Satisfiability Testing, 7th International Conference, {SAT} 2004, Vancouver, BC, Canada, May 10-13, 2004, Revised Selected Papers},
 series       = {Lecture Notes in Computer Science},
 volume       = {3542},
 publisher    = {Springer},
 pages        = {360--375},
 doi          = {10.1007/11527695\_27},
)
@inproceedings(DBLP:conf/lpar/PaulsonB10,
 author       = {Lawrence~C. Paulson and Jasmin~Christian Blanchette},
 year         = {2010},
 title        = {Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers},
 editor       = {Geoff Sutcliffe and Stephan Schulz and Eugenia Ternovska},
 booktitle    = {The 8th International Workshop on the Implementation of Logics, {IWIL} 2010, Yogyakarta, Indonesia, October 9, 2011},
 series       = {EPiC Series},
 volume       = {2},
 publisher    = {EasyChair},
 pages        = {1--11},
 url          = {http://www.easychair.org/publications/?page=820355915},
)
@article(DBLP:journals/fmsd/StumpORHT13,
 author       = {Aaron Stump and Duckki Oe and Andrew Reynolds and Liana Hadarean and Cesare Tinelli},
 year         = {2013},
 title        = {{SMT} proof checking using a logical framework},
 journal      = {Formal Methods in System Design},
 volume       = {42},
 number       = {1},
 pages        = {91--118},
 doi          = {10.1007/s10703-012-0163-3},
)
@inproceedings(Tseitin70,
 author       = {G.~Tseitin},
 year         = {1970},
 title        = {{On the Complexity of Proofs in Propositional Logics}},
 booktitle    = {Seminars in Mathematics},
 volume       = {8},
 pages        = {466--483},
)
@phdthesis(Weber08,
 author       = {T.~Weber},
 year         = {2008},
 title        = {{SAT-based Finite Model Generation for Higher-Order Logic}},
 school       = {Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen},
 address      = {Germany},
 url          = {http://www.cl.cam.ac.uk/~tw333/publications/weber08satbased.html},
)
@inproceedings(DBLP:conf/itp/WetzlerHH13,
 author       = {Nathan Wetzler and Marijn Heule and Warren A.~Hunt Jr.},
 year         = {2013},
 title        = {Mechanical Verification of {SAT} Refutations with Extended Resolution},
 editor       = {Sandrine Blazy and Paulin{-}Mohring, Christine and David Pichardie},
 booktitle    = {Interactive Theorem Proving - 4th International Conference, {ITP} 2013, Rennes, France, July 22-26, 2013. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {7998},
 publisher    = {Springer},
 pages        = {229--244},
 doi          = {10.1007/978-3-642-39634-2\_18},
)