@inbook(armand-et-al-2011, author = {Michael Armand and Germain Faure and Benjamin Gr{\'e}goire and Chantal Keller and Laurent Th{\'e}ry and Benjamin Werner}, year = {2011}, title = {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}, pages = {135--150}, publisher = {Springer Berlin Heidelberg}, address = {Berlin, Heidelberg}, url = {http://dx.doi.org/10.1007/978-3-642-25379-9_12}, ) @inproceedings(bobot-et-al-2011, author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and Claude March\'e and Andrei Paskevich}, year = {2011}, title = {{Why3}: Shepherd Your Herd of Provers}, editor = {K.~Rustan~M. Leino and Micha\l{} Moskal}, booktitle = {Boogie 2011}, pages = {53--64}, ) @inproceedings(brown-2012, author = {Chad~E. Brown}, year = {2012}, title = {Satallax: An Automatic Higher-Order Prover}, editor = {Bernhard Gramlich and Dale Miller and Uli Sattler}, booktitle = {Automated Reasoning---6th International Joint Conference, {IJCAR} 2012, Manchester, UK, June 26-29, 2012. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {7364}, publisher = {Springer}, pages = {111--117}, url = {http://dx.doi.org/10.1007/978-3-642-31365-3_11}, ) @inbook(corbineau-2004, author = {Pierre Corbineau}, year = {2004}, title = {First-Order Reasoning in the Calculus of Inductive Constructions}, pages = {162--177}, publisher = {Springer Berlin Heidelberg}, address = {Berlin, Heidelberg}, url = {http://dx.doi.org/10.1007/978-3-540-24849-1_11}, ) @article(kaliszyk-urban-2015, author = {Cezary Kaliszyk and Josef Urban}, year = {2015}, title = {{HOL(y)Hammer}: Online {ATP} Service for {HOL} {Light}}, journal = {Mathematics in Computer Science}, volume = {9}, number = {1}, pages = {5--22}, url = {http://dx.doi.org/10.1007/s11786-014-0182-0}, ) @inproceedings(Kaliszyk-2015, author = {Cezary Kaliszyk and Josef Urban and Vysko\v{c}il, Ji\v{r}i}, year = {2015}, title = {Certified Connection Tableaux Proofs for {HOL Light} and {TPTP}}, booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs}, series = {CPP '15}, publisher = {ACM}, address = {New York, NY, USA}, pages = {59--66}, url = {http://doi.acm.org/10.1145/2676724.2693176}, ) @inproceedings(otten-2005, author = {Jens Otten}, year = {2005}, title = {Clausal Connection-Based Theorem Proving in Intuitionistic First-Order Logic}, editor = {Bernhard Beckert}, booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods: 14th International Conference, TABLEAUX 2005, Koblenz, Germany, September 14-17, 2005. Proceedings}, publisher = {Springer Berlin Heidelberg}, address = {Berlin, Heidelberg}, pages = {245--261}, url = {http://dx.doi.org/10.1007/11554554_19}, ) @inproceedings(otten-2008, author = {Jens Otten}, year = {2008}, title = {{leanCoP} 2.0 and {ileanCoP} 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)}, editor = {Alessandro Armando and Peter Baumgartner and Gilles Dowek}, booktitle = {Automated Reasoning: 4th International Joint Conference, IJCAR 2008 Sydney, Australia, August 12-15, 2008 Proceedings}, publisher = {Springer Berlin Heidelberg}, address = {Berlin, Heidelberg}, pages = {283--291}, url = {http://dx.doi.org/10.1007/978-3-540-71070-7_23}, ) @misc(otten-2016-private, author = {Jens Otten}, year = {2016}, howpublished = {personal communication}, ) @inproceedings(otten-2016, author = {Jens Otten}, year = {2016}, title = {{nanoCoP}: A Non-clausal Connection Prover}, booktitle = {Automated Reasoning: 8th International Joint Conference, IJCAR 2016 Coimbra, Portugal, June 27 -July 2, 2016 Proceedings}, note = {To appear}, ) @inproceedings(paulson-blanchette-2010, author = {Lawrence~C. Paulson and Jasmin~Christian Blanchette}, year = {2010}, title = {Three years of experience with {Sledgehammer}, a Practical Link Between Automatic and Interactive Theorem Provers}, editor = {Geoff Sutcliffe and Stephan Schulz and Eugenia Ternovska}, booktitle = {The 8th International Workshop on the Implementation of Logics, {IWIL} 2010, Yogyakarta, Indonesia, October 9, 2011}, series = {EPiC Series}, volume = {2}, publisher = {EasyChair}, pages = {1--11}, url = {http://www.easychair.org/publications/?page=820355915}, ) @article(Rath-2007, author = {Thomas Raths and Jens Otten and Christoph Kreitz}, year = {2007}, title = {The {ILTP} Problem Library for Intuitionistic Logic: Release v1.1}, journal = {Journal of Automated Reasoning}, volume = {38}, number = {1-3}, pages = {261--271}, url = {http://dx.doi.org/10.1007/s10817-006-9060-z}, ) @inproceedings(Schmitt-1996, author = {Stephan Schmitt and Christoph Kreitz}, year = {1996}, title = {Converting non-classical matrix proofs into sequent-style systems}, booktitle = {Automated Deduction --- Cade-13: 13th International Conference on Automated Deduction New Brunswick, NJ, USA, July 30 -- August 3, 1996 Proceedings}, publisher = {Springer Berlin Heidelberg}, address = {Berlin, Heidelberg}, pages = {418--432}, url = {http://dx.doi.org/10.1007/3-540-61511-3_104}, ) @inproceedings(Schmitt-et-al-2001, author = {Stephan Schmitt and Lori Lorigo and Christoph Kreitz and Alexey Nogin}, year = {2001}, title = {{{ \sf JProver}} : Integrating Connection-based Theorem Proving into Interactive Proof Assistants}, editor = {R.~Gore and A.~Leitsch and T.~Nipkow}, booktitle = {International Joint Conference on Automated Reasoning}, series = {Lecture Notes in Artificial Intelligence}, volume = {2083}, publisher = {Springer Verlag}, pages = {421--426}, doi = {10.1007/3-540-45744-5\_34}, ) @book(Wallen-1990, author = {Lincoln Wallen}, year = {1990}, title = {Automated Deduction in Nonclassical Logics}, publisher = {MIT Press}, address = {Cambridge, MA, USA}, )