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 http://dx.doi.org/10.1007/978-3-642-25379-9_12.
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.
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 http://dx.doi.org/10.1007/978-3-642-31365-3_11.
Pierre Corbineau (2004):
First-Order Reasoning in the Calculus of Inductive Constructions,
pp. 162–177.
Springer Berlin Heidelberg,
Berlin, Heidelberg.
Available at http://dx.doi.org/10.1007/978-3-540-24849-1_11.
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 http://dx.doi.org/10.1007/s11786-014-0182-0.
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 http://doi.acm.org/10.1145/2676724.2693176.
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 http://dx.doi.org/10.1007/11554554_19.
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 http://dx.doi.org/10.1007/978-3-540-71070-7_23.
Jens Otten (2016).
personal communication.
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.
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.
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 http://dx.doi.org/10.1007/s10817-006-9060-z.
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 http://dx.doi.org/10.1007/3-540-61511-3_104.
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.
Lincoln Wallen (1990):
Automated Deduction in Nonclassical Logics.
MIT Press,
Cambridge, MA, USA.