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: Jouannaud & Shao,
pp. 135–150,
doi:10.1007/978-3-642-25379-9_12.
B. Barras, S. Boutin, C. Cornes, J. Courant, J.C. Filliâtre, E. Gimenez, H. Herbelin, G. Huet, C. Muñoz & C. Murthy (2000):
The Coq proof assistant: reference manual.
Technical Report.
INRIA.
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 - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings,
Lecture Notes in Computer Science 6806.
Springer,
pp. 171–177,
doi:10.1007/978-3-642-22110-1_14.
Clark Barrett, Aaron Stump & Cesare Tinelli (2010):
The SMT-LIB Standard: Version 2.0.
In: A. Gupta & D. Kroening: Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK).
F. Besson (2006):
Fast Reflexive Arithmetic Tactics the Linear Case and Beyond.
In: Thorsten Altenkirch & Conor McBride: TYPES,
Lecture Notes in Computer Science 4502.
Springer,
pp. 48–62,
doi:10.1007/978-3-540-74464-1_4.
F. Besson, P. Fontaine & L. Théry (2011):
A Flexible Proof Format for SMT: a Proposal.
In: PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving August 1, 2011 Affiliated with CADE 2011, 31 July-5 August 2011 Wrocław, Poland,
pp. 15–26.
Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson & Josef Urban (2016):
Hammering towards QED.
J. Formalized Reasoning 9(1),
pp. 101–148,
doi:10.6092/issn.1972-5787/4593.
Sascha Böhme, Anthony C. J. Fox, Thomas Sewell & Tjark Weber (2011):
Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL.
In: Jouannaud & Shao,
pp. 183–198,
doi:10.1007/978-3-642-25379-9_15.
Sascha Böhme & Tjark Weber (2010):
Fast LCF-Style Proof Reconstruction for Z3.
In: Matt Kaufmann & Lawrence C. Paulson: Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings,
Lecture Notes in Computer Science 6172.
Springer,
pp. 179–194,
doi:10.1007/978-3-642-14052-5_14.
T. Bouton, D.C.B. de Oliveira, D. Déharbe & P. Fontaine (2009):
veriT: An Open, Trustable and Efficient SMT-Solver.
In: R. A. Schmidt: CADE,
Lecture Notes in Computer Science 5663.
Springer,
pp. 151–156,
doi:10.1007/978-3-642-02959-2_12.
Allen Van Gelder (2012):
Producing and verifying extremely large propositional refutations - Have your cake and eat it too.
Ann. Math. Artif. Intell. 65(4),
pp. 329–372,
doi:10.1007/s10472-012-9322-x.
Georges Gonthier & Assia Mahboubi (2010):
An introduction to small scale reflection in Coq.
J. Formalized Reasoning 3(2),
pp. 95–152,
doi:10.6092/issn.1972-5787/1979.
Liana Hadarean, Clark W. Barrett, Andrew Reynolds, Cesare Tinelli & Morgan Deters (2015):
Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors.
In: Martin Davis, Ansgar Fehnker, Annabelle McIver & Andrei Voronkov: Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings,
Lecture Notes in Computer Science 9450.
Springer,
pp. 340–355,
doi:10.1007/978-3-662-48899-7_24.
Robert Harper, Furio Honsell & Gordon D. Plotkin (1993):
A Framework for Defining Logics.
J. ACM 40(1),
pp. 143–184,
doi:10.1145/138027.138060.
Marijn Heule, Warren A. Hunt Jr. & Nathan Wetzler (2013):
Verifying Refutations with Extended Resolution.
In: Maria Paola Bonacina: Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings,
Lecture Notes in Computer Science 7898.
Springer,
pp. 345–359,
doi:10.1007/978-3-642-38574-2_24.
Jean-Pierre Jouannaud & Zhong Shao (2011):
Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings.
Lecture Notes in Computer Science 7086.
Springer,
doi:10.1007/978-3-642-25379-9.
Oliver Kullmann (1999):
On a Generalization of Extended Resolution.
Discrete Applied Mathematics 96-97,
pp. 149–176,
doi:10.1016/S0166-218X(99)00037-2.
Pierre Letouzey (2002):
A New Extraction for Coq.
In: Herman Geuvers & Freek Wiedijk: Types for Proofs and Programs, Second International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, Selected Papers,
Lecture Notes in Computer Science 2646.
Springer,
pp. 200–219,
doi:10.1007/3-540-39185-1_12.
Yogesh S. Mahajan, Zhaohui Fu & Sharad Malik (2004):
Zchaff2004: An Efficient SAT Solver.
In: Holger H. Hoos & David G. Mitchell: Theory and Applications of Satisfiability Testing, 7th International Conference, SAT 2004, Vancouver, BC, Canada, May 10-13, 2004, Revised Selected Papers,
Lecture Notes in Computer Science 3542.
Springer,
pp. 360–375,
doi:10.1007/11527695_27.
Lawrence C. Paulson & Jasmin Christian Blanchette (2010):
Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers.
In: Geoff Sutcliffe, Stephan Schulz & Eugenia Ternovska: The 8th International Workshop on the Implementation of Logics, IWIL 2010, Yogyakarta, Indonesia, October 9, 2011,
EPiC Series 2.
EasyChair,
pp. 1–11.
Available at http://www.easychair.org/publications/?page=820355915.
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.
G. Tseitin (1970):
On the Complexity of Proofs in Propositional Logics.
In: Seminars in Mathematics 8,
pp. 466–483.
Nathan Wetzler, Marijn Heule & Warren A. Hunt Jr. (2013):
Mechanical Verification of SAT Refutations with Extended Resolution.
In: Sandrine Blazy, Christine Paulin-Mohring & David Pichardie: Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings,
Lecture Notes in Computer Science 7998.
Springer,
pp. 229–244,
doi:10.1007/978-3-642-39634-2_18.