References

  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 http://www.easychair.org/publications/?page=820355915.
  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 http://www.cl.cam.ac.uk/~tw333/publications/weber08satbased.html.
  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: eptcs@eptcs.org
For website issues: webmaster@eptcs.org