1. Michael Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry & Benjamin Werner (2011): Certified Programs and Proofs: First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings, chapter A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses, pp. 135–150. Springer Berlin Heidelberg, Berlin, Heidelberg. Available at
  2. François Bobot, Jean-Christophe Filliâtre, Claude Marché & Andrei Paskevich (2011): Why3: Shepherd Your Herd of Provers. In: K. Rustan M. Leino & MichałMoskal: Boogie 2011, pp. 53–64.
  3. Chad E. Brown (2012): Satallax: An Automatic Higher-Order Prover. In: Bernhard Gramlich, Dale Miller & Uli Sattler: Automated Reasoning—6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings, Lecture Notes in Computer Science 7364. Springer, pp. 111–117. Available at
  4. Pierre Corbineau (2004): First-Order Reasoning in the Calculus of Inductive Constructions, pp. 162–177. Springer Berlin Heidelberg, Berlin, Heidelberg. Available at
  5. Cezary Kaliszyk & Josef Urban (2015): HOL(y)Hammer: Online ATP Service for HOL Light. Mathematics in Computer Science 9(1), pp. 5–22. Available at
  6. Cezary Kaliszyk, Josef Urban & Jiři Vyskočil (2015): Certified Connection Tableaux Proofs for HOL Light and TPTP. In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP '15. ACM, New York, NY, USA, pp. 59–66. Available at
  7. Jens Otten (2005): Clausal Connection-Based Theorem Proving in Intuitionistic First-Order Logic. In: Bernhard Beckert: Automated Reasoning with Analytic Tableaux and Related Methods: 14th International Conference, TABLEAUX 2005, Koblenz, Germany, September 14-17, 2005. Proceedings. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 245–261. Available at
  8. Jens Otten (2008): leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions). In: Alessandro Armando, Peter Baumgartner & Gilles Dowek: Automated Reasoning: 4th International Joint Conference, IJCAR 2008 Sydney, Australia, August 12-15, 2008 Proceedings. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 283–291. Available at
  9. Jens Otten (2016). personal communication.
  10. Jens Otten (2016): nanoCoP: A Non-clausal Connection Prover. In: Automated Reasoning: 8th International Joint Conference, IJCAR 2016 Coimbra, Portugal, June 27 -July 2, 2016 Proceedings. To appear.
  11. 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
  12. Thomas Raths, Jens Otten & Christoph Kreitz (2007): The ILTP Problem Library for Intuitionistic Logic: Release v1.1. Journal of Automated Reasoning 38(1-3), pp. 261–271. Available at
  13. Stephan Schmitt & Christoph Kreitz (1996): Converting non-classical matrix proofs into sequent-style systems. In: Automated Deduction — Cade-13: 13th International Conference on Automated Deduction New Brunswick, NJ, USA, July 30 – August 3, 1996 Proceedings. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 418–432. Available at
  14. Stephan Schmitt, Lori Lorigo, Christoph Kreitz & Alexey Nogin (2001): JProver : Integrating Connection-based Theorem Proving into Interactive Proof Assistants. In: R. Gore, A. Leitsch & T. Nipkow: International Joint Conference on Automated Reasoning, Lecture Notes in Artificial Intelligence 2083. Springer Verlag, pp. 421–426, doi:10.1007/3-540-45744-5_34.
  15. Lincoln Wallen (1990): Automated Deduction in Nonclassical Logics. MIT Press, Cambridge, MA, USA.

Comments and questions to:
For website issues: