1. 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.
  2. 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.
  3. 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.
  4. 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).
  5. 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.
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. 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.
  11. 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.
  12. 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.
  13. 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.
  14. 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.
  15. 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.
  16. 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.
  17. 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.
  18. 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.
  19. 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.
  20. 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
  21. 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.
  22. G. Tseitin (1970): On the Complexity of Proofs in Propositional Logics. In: Seminars in Mathematics 8, pp. 466–483.
  23. T. Weber (2008): SAT-based Finite Model Generation for Higher-Order Logic. Institut für Informatik, Technische Universität München, Germany. Available at
  24. 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.

Comments and questions to:
For website issues: