@incollection(Satallax, author = {J. Backes and C.E. Brown}, year = {2010}, title = {Analytic Tableaux for Higher-Order Logic with Choice}, editor = {J. Giesl and R. H{\"a}hnle}, booktitle = {Automated Reasoning}, series = {Lecture Notes in Computer Science}, volume = {6173}, publisher = {Springer Berlin Heidelberg}, pages = {76--90}, doi = {10.1007/978-3-642-14203-1\_7}, ) @incollection(CVC4, author = {C. Barrett and C.L. Conway and M. Deters and L. Hadarean and D. Jovanovic and T. King and A. Reynolds and C. Tinelli}, year = {2011}, title = {CVC4}, editor = {Ganesh Gopalakrishnan and Shaz Qadeer}, booktitle = {Computer Aided Verification}, series = {LNCS}, volume = {6806}, publisher = {Springer Berlin Heidelberg}, pages = {171--177}, doi = {10.1007/978-3-642-22110-1\_14}, ) @incollection(B12, author = {C. Benzm\"uller}, year = {2010}, title = {Verifying the Modal Logic Cube is an Easy Task (for Higher-Order Automated Reasoners)}, editor = {S. Siegler and N. Wasser}, booktitle = {Verification, Induction, Termination Analysis - Festschrift for Christoph Walther on the Occasion of His 60th Birthday}, series = {LNCS}, volume = {6463}, publisher = {Springer}, pages = {117--128}, doi = {10.1007/978-3-642-17172-7\_7}, url = {http://christoph-benzmueller.de/papers/B12.pdf}, ) @inproceedings(IJCAI, author = {C. Benzm{\"u}ller}, year = {2013}, title = {Automating Quantified Conditional Logics in {HOL}}, editor = {F. Rossi}, booktitle = {23rd International Joint Conference on Artificial Intelligence (IJCAI-13)}, address = {Beijing, China}, pages = {746--753}, url = {http://ijcai.org/papers13/Papers/IJCAI13-117.pdf}, ) @article(GoedelGod-AFP, author = {C. Benzm\"uller and B. Woltzenlogel Paleo}, year = {2013}, title = {G\"odel's God in Isabelle/HOL}, journal = {Archive of Formal Proofs}, note = {\url{http://afp.sf.net/entries/GoedelGod.shtml}, Formal proof development}, ) @inproceedings(ECAI, author = {C. Benzm{\"u}ller and B. Woltzenlogel Paleo}, year = {2014}, title = {Automating {G\"{o}del's} Ontological Proof of {God}'s Existence with Higher-order Automated Theorem Provers}, editor = {T. Schaub and G. Friedrich and B. O'Sullivan}, booktitle = {ECAI 2014}, series = {Frontiers in Artificial Intelligence and Applications}, volume = {263}, publisher = {IOS Press}, pages = {93 -- 98}, doi = {10.3233/978-1-61499-419-0-93}, url = {http://christoph-benzmueller.de/papers/C40.pdf}, ) @article(J23, author = {C. Benzm{\"u}ller and L.C. Paulson}, year = {2013}, title = {Quantified Multimodal Logics in Simple Type Theory}, journal = {Logica Universalis (Special Issue on Multimodal Logics)}, volume = {7}, number = {1}, pages = {7--20}, doi = {10.1007/s11787-012-0052-y}, url = {http://christoph-benzmueller.de/papers/J23.pdf}, ) @inproceedings(C25, author = {C. Benzm{\"u}ller and F. Rabe and G. Sutcliffe}, year = {2008}, title = {{THF0} -- The Core of the {TPTP} Language for Classical Higher-Order Logic}, editor = {A. Armando and P. Baumgartner and G. Dowek}, booktitle = {Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings}, series = {LNCS}, volume = {5195}, publisher = {Springer}, pages = {491--506}, doi = {10.1007/978-3-540-71070-7\_41}, url = {http://christoph-benzmueller.de/papers/C25.pdf}, ) @inproceedings(C26, author = {C. Benzm{\"u}ller and F. Theiss and L.C. Paulson and A. Fietzke}, year = {2008}, title = {{LEO-II} - A Cooperative Automatic Theorem Prover for Higher-Order Logic (System Description)}, editor = {A. Armando and P. Baumgartner and G. Dowek}, booktitle = {Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings}, series = {LNCS}, volume = {5195}, publisher = {Springer}, pages = {162--170}, doi = {10.1007/978-3-540-71070-7\_14}, url = {http://christoph-benzmueller.de/papers/C26.pdf}, ) @inproceedings(BlanchetteN-ITP10, author = {J.C. Blanchette and T. Nipkow}, year = {2010}, title = {Nitpick: A counterexample generator for higher-order logic based on a relational model finder}, editor = {M. Kaufmann and L. Paulson}, booktitle = {Interactive Theorem Proving (ITP 2010)}, volume = {6172}, pages = {131--146}, doi = {10.1007/978-3-642-14052-5\_11}, ) @inproceedings(hurd2003d, author = {J. Hurd}, year = {2003}, title = {First-Order Proof Tactics in Higher-Order Logic Theorem Provers}, editor = {M. Archer and B. Di Vito and Mu{\~{n}}oz, C.}, booktitle = {Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003)}, series = {{NASA} Technical Reports}, pages = {56--68}, url = {http://www.gilith.com/research/papers}, ) @inproceedings(Vampire, author = {L. Kov{\'{a}}cs and A. Voronkov}, year = {2013}, title = {First-Order Theorem Proving and Vampire}, editor = {N. Sharygina and H. Veith}, booktitle = {Computer Aided Verification - 25th International Conference, {CAV} 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings}, series = {LNCS}, volume = {8044}, publisher = {Springer}, pages = {1--35}, doi = {10.1007/978-3-642-39799-8\_1}, ) @inproceedings(Z3, author = {L.M. de Moura and Bj{\o}rner, N.}, year = {2008}, title = {{Z3:} An Efficient {SMT} Solver}, editor = {C.R. Ramakrishnan and J. Rehof}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, {TACAS} 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings}, series = {LNCS}, volume = {4963}, publisher = {Springer}, pages = {337--340}, doi = {10.1007/978-3-540-78800-3\_24}, ) @book(Nipkow-Paulson-Wenzel:2002, author = {T. Nipkow and L.C. Paulson and M. Wenzel}, year = {2002}, title = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic}, series = {LNCS}, volume = {2283}, publisher = {Springer}, ) @inproceedings(EasyChair:128, author = {L.C. Paulson and J.C. Blanchette}, year = {2012}, title = {Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers}, editor = {G. Sutcliffe and S. Schulz and E. Ternovska}, booktitle = {IWIL 2010}, series = {EPiC Series}, volume = {2}, publisher = {EasyChair}, pages = {1--11}, ) @article(Rabe, author = {F. Rabe and P. Pudlak and G. Sutcliffe and W. Shen}, year = {2009}, title = {Solving the \$ 100 modal logic challenge}, journal = {Journal of Applied Logic}, volume = {7}, pages = {113--130}, doi = {10.1016/j.jal.2007.07.007}, ) @inproceedings(E, author = {S. Schulz}, year = {2013}, title = {System Description: {E} 1.8}, editor = {K.L. McMillan and A. Middeldorp and A. Voronkov}, booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings}, series = {LNCS}, volume = {8312}, publisher = {Springer}, pages = {735--743}, doi = {10.1007/978-3-642-45221-5\_49}, ) @phdthesis(sultana14:_higher, author = {N. Sultana}, year = {2015}, title = {{Higher-order proof translation}}, school = {Computer Laboratory, University of Cambridge}, note = {Available as Tech Report UCAM-CL-TR-867}, ) @inproceedings(SPASS, author = {C. Weidenbach and D. Dimova and A. Fietzke and R. Kumar and M. Suda and P. Wischnewski}, year = {2009}, title = {{SPASS} Version 3.5}, editor = {R.A. Schmidt}, booktitle = {Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings}, series = {LNCS}, volume = {5663}, publisher = {Springer}, pages = {140--145}, doi = {10.1007/978-3-642-02959-2\_10}, )