@inproceedings{IsabelleJEDIT,
  author    = {Makarius Wenzel},
  editor    = {Johan Jeuring and
               John A. Campbell and
               Jacques Carette and
               Gabriel Dos Reis and
               Petr Sojka and
               Makarius Wenzel and
               Volker Sorge},
  title     = {Isabelle/jEdit - {A} Prover {IDE} within the {PIDE} Framework},
  booktitle = {Intelligent Computer Mathematics - 11th International Conference,
               {AISC} 2012, 19th Symposium, Calculemus 2012, 5th International Workshop,
               {DML} 2012, 11th International Conference, {MKM} 2012, Systems and
               Projects, Held as Part of {CICM} 2012, Bremen, Germany, July 8-13,
               2012. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {7362},
  pages     = {468--471},
  publisher = {Springer},
  year      = {2012},
  url       = {https://doi.org/10.1007/978-3-642-31374-5\_38},
  doi       = {10.1007/978-3-642-31374-5\_38},
  timestamp = {Sun, 02 Jun 2019 21:23:46 +0200},
  biburl    = {https://dblp.org/rec/conf/aisc/Wenzel12.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}


@article{Sledgehammer,
  title={Hammering towards {QED}},
  author={Blanchette, Jasmin C. and Kaliszyk, Cezary and Paulson, Lawrence C. and Urban, Josef},
  journal={Journal of Formalized Reasoning},
  volume={9},
  number={1},
  pages={101--148},
  year={2016}
}


@inproceedings{Z3,
  author    = {Leonardo Mendon{\c{c}}a de Moura and
               Nikolaj S. Bj{\o}rner},
  editor    = {C. R. Ramakrishnan and
               Jakob Rehof},
  title     = {{Z3:} An Efficient {SMT} Solver},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems,
               14th International Conference, {TACAS} 2008, Held as Part of the Joint
               European Conferences on Theory and Practice of Software, {ETAPS} 2008,
               Budapest, Hungary, March 29-April 6, 2008. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {4963},
  pages     = {337--340},
  publisher = {Springer},
  year      = {2008},
  url       = {https://doi.org/10.1007/978-3-540-78800-3\_24},
  doi       = {10.1007/978-3-540-78800-3\_24},
  timestamp = {Thu, 14 Apr 2022 20:26:15 +0200},
  biburl    = {https://dblp.org/rec/conf/tacas/MouraB08.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}


@inproceedings{Vampire,
 author = {Kotelnikov, Evgenii and Kov\'{a}cs, Laura and Reger, Giles and Voronkov, Andrei},
 title = {The Vampire and the FOOL},
 booktitle = {Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs},
 series = {CPP 2016},
 year = {2016},
 location = {St. Petersburg, FL, USA},
 pages = {37--48},
 numpages = {12},
 publisher = {ACM},
} 


@article{J63,
  OPtdoi = {},
  author = {Benzmüller, Christoph and Fuenmayor, David and Steen, Alexander and Sutcliffe, Geoff},
  title =	 {Who Finds the Short Proof? An Exploration of Variants of {Boolos' Curious Inference} using Higher-order Automated Theorem Provers},
  journal =	 {Logic Journal of the IGPL},
  OPTnumber =	 {},
  OPTvolume =	 {},
  year =	 2023,
  note =	 {In print; arXiv preprint: \url{http://doi.org/10.48550/arXiv.2208.06879}},
}

@inproceedings{HeuleKB17,
  author    = {Marijn J. H. Heule and
               Benjamin Kiesl and
               Armin Biere},
  editor    = {Leonardo de Moura},
  title     = {Short Proofs Without New Variables},
  booktitle = {Automated Deduction - {CADE} 26 - 26th International Conference on
               Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {10395},
  pages     = {130--147},
  publisher = {Springer},
  address   = {Cham},
  year      = {2017},
  doi       = {10.1007/978-3-319-63046-5\_9},
  timestamp = {Thu, 29 Sep 2022 08:36:56 +0200},
  biburl    = {https://dblp.org/rec/conf/cade/HeuleKB17.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@book{ComputationalLogic,
  author    = {Boyer, Robert S. and Moore, J. Strother},
  title     = {A computational logic},
  series    = {{ACM} monograph series},
  publisher = {Academic Press},
  address   = {London},
  year      = {1979}
}

@article{BoolosCut,
	year = {1984},
	number = {4},
	author = {George Boolos},
	publisher = {Springer},
	title = {Don't Eliminate Cut},
	doi = {10.1007/BF00247711},
	pages = {373--378},
	journal = {Journal of Philosophical Logic},
	volume = {13}
}

@InProceedings{SST14old,
  Author =	 {Stump, A. and Sutcliffe, G. and Tinelli, C.},
  Year =	 2014,
  Title =	 {{StarExec}: {A} Cross-Community Infrastructure for
                  Logic Solving},
  Editor =	 {Demri, S. and Kapur, D. and Weidenbach, C.},
  optbooktitle =    {{IJCAR} 2014}, 
  BookTitle =	 {Proceedings of the 7th International Joint
                  Conference on Automated Reasoning},
  Series =	 {Lecture Notes in Artificial Intelligence},
  Number =	 8562,
  Pages =	 {367-373},
  Publisher = {Springer},
}

@inproceedings{SST14,
  author    = {Aaron Stump and
               Geoff Sutcliffe and
               Cesare Tinelli},
  editor    = {St{\'{e}}phane Demri and
               Deepak Kapur and
               Christoph Weidenbach},
  title     = {{StarExec}: {A} Cross-Community Infrastructure for Logic Solving},
  booktitle = {Automated Reasoning - 7th International Joint Conference, {IJCAR}
               2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,
               Austria, July 19-22, 2014. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {8562},
  pages     = {367--373},
  publisher = {Springer},
  address = {Cham},
  year      = {2014},
  opturl       = {https://doi.org/10.1007/978-3-319-08587-6_28},
  doi       = {10.1007/978-3-319-08587-6_28},
  timestamp = {Fri, 09 Apr 2021 18:50:53 +0200},
  biburl    = {https://dblp.org/rec/conf/cade/StumpST14.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@Article{Sut22-IGPL,
  Author =	 {Sutcliffe, Geoff},
  Year =	 2022,
  Title =	 {The Logic Languages of the {TPTP} World},
  Journal = {Logic Journal of the IGPL},
  url =		 {https://doi.org/10.1093/jigpal/jzac068},
  doi =		 {10.1093/jigpal/jzac068},  
  Comment =	 "TPTPCite"
}

@InProceedings{SB18,
  Author =	 {Steen, Alexander and Benzm{\"u}ller, Christoph},
  Year =	 2018,
  Title =	 {The Higher-Order Prover {Leo-III}},
  Editor =	 {Galmiche, D. and Schulz, S. and Sebastiani, R.},
  BookTitle = {Proceedings of the 8th International Joint
                  Conference on Automated Reasoning},
  Series =	 {Lecture Notes in Artificial Intelligence},
  Number =	 10900,
  Pages =	 {108-116},
  Publisher = {Springer},
}

@InProceedings{KV13old,
  Author =	 {Kovacs, Laura and Voronkov, Andrei},
  Year =	 2013,
  Title =	 {First-Order Theorem Proving and {Vampire}},
  Editor =	 {Sharygina, N. and Veith, H.},
  BookTitle = {Proceedings of the 25th International Conference on
                  Computer Aided Verification},
  optBooktitle = {{CAV} 2013},
  Series =	 {Lecture Notes in Artificial Intelligence},
  Number =	 8044,
  Pages =	 {1-35},
  Publisher =	 {Springer},
}

@inproceedings{KV13,
  author    = {Laura Kov{\'{a}}cs and
               Andrei Voronkov},
  editor    = {Natasha Sharygina and
               Helmut Veith},
  title     = {First-Order Theorem Proving and {Vampire}},
  booktitle = {Computer Aided Verification - 25th International Conference, {CAV}
               2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {8044},
  pages     = {1--35},
  publisher = {Springer},
  address = {Berlin, Heidelberg},
  year      = {2013},
  opturl       = {https://doi.org/10.1007/978-3-642-39799-8_1},
  doi       = {10.1007/978-3-642-39799-8_1},
  timestamp = {Tue, 14 May 2019 10:00:43 +0200},
  biburl    = {https://dblp.org/rec/conf/cav/KovacsV13.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}


@incollection{BoolosOmegaMizar,
  Author =	 {Christoph Benzm{\"u}ller and Chad Brown},
  Booktitle =	 {From Insight to Proof -- Festschrift in Honour of
                  {Andrzej} {Trybulec}},
  Editor =	 {Roman Matuszewski and Anna Zalewska},
  Isbn =	 {978-83-7431-128-1},
  Keywords =	 {own, Proof Assistants, OMEGA, Interactive Proof,
                  Higher Order Logic},
  Pages =	 {299-388},
  Publisher =	 {The University of Bialystok},
  address = {Poland},
  OPTurl = {http://mizar.org/trybulec65/book.pdf},
  Series =	 {Studies in Logic, Grammar, and Rhetoric},
  Title =	 {The curious inference of {B}oolos in {MIZAR} and
                  {OMEGA}},
  url_preprint = {http://christoph-benzmueller.de/papers/B6.pdf},
  Volume =	 {10(23)},
  Year =	 2007,
  note = {\href{http://mizar.org/trybulec65/20.pdf}{http://mizar.org/trybulec65/20.pdf}},
}

@inproceedings{LostProof,
  Address =	 {Siena, Italy},
  Author =	 {Christoph Benzm{\"u}ller and Manfred Kerber},
  Booktitle =	 {Proceedings of the IJCAR 2001 Workshop: Future
                  Directions in Automated Reasoning},
  Pages =	 {13-24},
  Title =	 {A Lost Proof},
  url_preprint = {http://christoph-benzmueller.de/papers/W13.pdf},
  url = {https://www.inf.ed.ac.uk/publications/online/0046/b040.pdf},
  Year =	 2001,
}

@article{BCI,
  author =	 {George Boolos},
  title =	 {A curious inference},
  journal =	 {J. Philos. Log.},
  volume =	 16,
  number =	 1,
  pages =	 {1--12},
  year =	 1987,
  url =		 {https://doi.org/10.1007/BF00250612},
  doi =		 {10.1007/BF00250612},
  timestamp =	 {Mon, 11 May 2020 23:01:28 +0200},
  biburl =	 {https://dblp.org/rec/journals/jphil/Boolos87.bib},
  bibsource =	 {dblp computer science bibliography,
                  https://dblp.org}
}

@article{ackermann1928,
  title =	 "{Zum Hilbertschen Aufbau der reellen Zahlen}",
  author =	 {Ackermann, Wilhelm},
  journal =	 {Mathematische Annalen},
  volume =	 99,
  number =	 1,
  pages =	 {118--133},
  year =	 1928,
  doi =      {10.1007/BF01459088},
  publisher =	 {Springer-Verlag}
}

@article{KetlandAFP,
  author =	 {Jeffrey Ketland},
  title =	 {Boolos's Curious Inference in {Isabelle/HOL}},
  journal =	 {Archive of Formal Proofs},
  month =	 {June},
  year =	 2022,
  pages =        {1-19},
  url =
                  {https://isa-afp.org/entries/Boolos_Curious_Inference.html},
  ISSN =	 {2150-914x},
  note    = {\href{https://isa-afp.org/entries/Boolos_Curious_Inference.html}{https://isa-afp.org/entries/Boolos\_Curious\_Inference.html}},
}

@book{AndrewsOld,
  author =	 {Peter B. Andrews},
  title =	 {An Introduction to Mathematical Logic and Type Theory -- To Truth Through Proof},
  series =	 {Computer science and applied mathematics},
  publisher =	 {Academic Press},
  year =	 1986,
  isbn =	 {978-0-12-058535-9},
  timestamp =	 {Thu, 14 Apr 2011 14:43:25 +0200},
  biburl =	 {https://dblp.org/rec/books/daglib/0070479.bib},
  bibsource =	 {dblp computer science bibliography,
                  https://dblp.org}
}


@book{Andrews,
  title={An Introduction to Mathematical Logic and Type Theory},
  author={Andrews, P.B.},
  isbn={9781402007637},
  lccn={2002031656},
  doi = {10.1007/978-94-015-9934-4},
  series={Applied Logic Series},
  opturl={https://books.google.de/books?id=nV4zAsWAvT0C},
  year={2002},
  publisher={Springer},
  address = {Netherlands}
}


@inproceedings{Eprover,
  author =	 {Stephan Schulz and Simon Cruanes and Petar
                  Vukmirovic},
  editor =	 {Pascal Fontaine},
  title =	 {Faster, Higher, Stronger: {E} 2.3},
  optbooktitle = "{Automated Deduction - {CADE} 27 - 27th International
                  Conference on Automated Deduction, Natal, Brazil,
                  August 27-30, 2019, Proceedings}",
  booktitle =    {{CADE} 2019},		  
  series =	 {Lecture Notes in Computer Science},
  volume =	 11716,
  pages =	 {495--507},
  publisher =	 {Springer},
  address  = {Cham},
  year =	 2019,
  opturl =		 {https://doi.org/10.1007/978-3-030-29436-6_29},
  doi =		 {10.1007/978-3-030-29436-6_29},
  timestamp =	 {Sat, 19 Oct 2019 20:28:03 +0200},
  biburl =	 {https://dblp.org/rec/conf/cade/0001CV19.bib},
  bibsource =	 {dblp computer science bibliography,
                  https://dblp.org}
}

@InCollection{GoedelProofLength,
  title =	 {{Über die Länge von Beweisen}},
  author =	 {Kurt Gödel},
  booktitle = {{Ergebnisse} eines mathematischen {Kolloquiums}: {Heft} x7: 1934-1935},
  editor =	 {Menger, K. and G{\"o}del, K. and Wald, A.},
  opturl =		 {https://books.google.de/books?id=BENTtQEACAAJ},
  year =	 1936,
  pages =	 {23–24},
  publisher =	 {Franz Deuticke},
  address  = {Vienna}
}

@incollection{Omega,
  Author =	 {Serge Autexier and Christoph Benzm{\"u}ller and
                  Dominik Dietrich and J\"org Siekmann},
  Booktitle =	 {Resource-Adaptive Cognitive Processes},
  Doi =		 {10.1007/978-3-540-89408-7_17},
  Editor =	 {Matthew W. Crocker and J\"org Siekmann},
  Isbn =	 {978-3-540-89407-0},
  Keywords =	 {own, Proof Assistants, OMEGA, Interactive Proof,
                  Automated Reasoning, Proof Planning, System
                  Integration, Agents},
  optNote =	 {(Final project report, DFG SFB 378)},
  Pages =	 {389-423},
  Publisher =	 {Springer},
  address = {Berlin, Heidelberg},
  Series =	 {Cognitive Technologies},
  Title =	 {{OMEGA}: Resource-Adaptive Processes in an Automated
                  Reasoning Systems},
  year =	 2010,
}

@inproceedings{Mizar,
  author =	 {Grzegorz Bancerek and Czeslaw Bylinski and Adam
                  Grabowski and Artur Kornilowicz and Roman
                  Matuszewski and Adam Naumowicz and Karol Pak and
                  Josef Urban},
  editor =	 {Manfred Kerber and Jacques Carette and Cezary
                  Kaliszyk and Florian Rabe and Volker Sorge},
  title =	 {Mizar: State-of-the-art and Beyond},
  booktitle = {Intelligent Computer Mathematics - International
                  Conference, {CICM} 2015, Washington, DC, USA, July
                  13-17, 2015, Proceedings},
  optbooktitle =    {{CICM 2015}},		  
  series =	 {Lecture Notes in Computer Science},
  volume =	 9150,
  pages =	 {261--279},
  publisher =	 {Springer},
  address = {Cham},
  year =	 2015,
  opturl =		 {https://doi.org/10.1007/978-3-319-20615-8_17},
  doi =		 {10.1007/978-3-319-20615-8_17},
  timestamp =	 {Fri, 20 Nov 2020 16:08:54 +0100},
  biburl =	 {https://dblp.org/rec/conf/mkm/BancerekBGKMNPU15.bib},
  bibsource =	 {dblp computer science bibliography,
                  https://dblp.org}
}

@book{Isabelle,
  author =	 {Tobias Nipkow and Lawrence C. Paulson and Markus
                  Wenzel},
  title =	 {{Isabelle/HOL} - {A} Proof Assistant for Higher-Order
                  Logic},
  series =	 {Lecture Notes in Computer Science},
  volume =	 2283,
  publisher =	 {Springer},
  address = {Berlin, Heidelberg},
  year =	 2002,
  opturl =		 {https://doi.org/10.1007/3-540-45949-9},
  doi =		 {10.1007/3-540-45949-9},
  isbn =	 {3-540-43376-7},
  timestamp =	 {Tue, 14 May 2019 10:00:35 +0200},
  biburl =	 {https://dblp.org/rec/books/sp/NipkowPW02.bib},
  bibsource =	 {dblp computer science bibliography,
                  https://dblp.org}
}

@article{THF,
  Author =	 {Geoff Sutcliffe and Christoph Benzm{\"u}ller},
  Issn =	 {1972-5787},
  Journal =	 {Journal of Formalized Reasoning},
  Keywords =	 {own, Higher Order Logic, Automated Reasoning, Henkin
                  Semantics},
  Number =	 1,
  Pages =	 {1-27},
  Title =	 {Automated Reasoning in Higher-Order Logic using the
                  {TPTP THF} Infrastructure},
  url_preprint = {https://www.researchgate.net/publication/49595291},
  opturl =		 {https://jfr.unibo.it/article/view/1710},
  Volume =	 3,
  Year =	 2010,
  doi = {10.6092/issn.1972-5787/1710},
}

@inproceedings{ScienceOfReasoning,
  author =	 {Alan Bundy},
  editor =	 {Jean{-}Louis Lassez and Gordon D. Plotkin},
  title =	 {A Science of Reasoning},
  booktitle =	 {Computational Logic - Essays in Honor of Alan
                  Robinson},
  pages =	 {178--198},
  publisher =	 {The {MIT} Press},
  address = {Cambridge, MA, USA},
  year =	 1991,
  note = {\href{https://mitpress.mit.edu/9780262121569/}{https://mitpress.mit.edu/9780262121569/}},                
}

@article{SiekmannMelis,
  author =	 {Erica Melis and J{\"{o}}rg H. Siekmann},
  title =	 {Knowledge-Based Proof Planning},
  journal =	 {Artificial Intelligence},
  volume =	 115,
  number =	 1,
  pages =	 {65--105},
  year =	 1999,
  opturl =		 {https://doi.org/10.1016/S0004-3702(99)00076-4},
  doi =		 {10.1016/S0004-3702(99)00076-4},
  timestamp =	 {Sat, 27 May 2017 14:24:42 +0200},
  biburl =	 {https://dblp.org/rec/journals/ai/MelisS99.bib},
  bibsource =	 {dblp computer science bibliography,
                  https://dblp.org}
}

@article{Leo3,
  Author =	 {Steen, Alexander and Benzm{\"u}ller, Christoph},
  title =	 {Extensional Higher-Order Paramodulation in {Leo-III}},
  journal =	 {Journal of Automated Reasoning},
  volume =	 65,
  number =	 6,
  pages =	 {775--807},
  year =	 2021,
  url =		 {https://doi.org/10.1007/s10817-021-09588-x},
  doi =		 {10.1007/s10817-021-09588-x}
}

@inproceedings{CVC5,
  author =	 {Haniel Barbosa and Clark W. Barrett and Martin Brain
                  and Gereon Kremer and Hanna Lachnitt and Makai Mann
                  and Abdalrhman Mohamed and Mudathir Mohamed and Aina
                  Niemetz and Andres N{\"{o}}tzli and Alex Ozdemir and
                  Mathias Preiner and Andrew Reynolds and Ying Sheng
                  and Cesare Tinelli and Yoni Zohar},
  editor =	 {Dana Fisman and Grigore Rosu},
  title =	 {cvc5: {A} Versatile and Industrial-Strength {SMT}
                  Solver},
  booktitle = {Tools and Algorithms for the Construction and
                  Analysis of Systems - 28th International Conference,
                  {TACAS} 2022, Held as Part of the European Joint
                  Conferences on Theory and Practice of Software,
                  {ETAPS} 2022, Munich, Germany, April 2-7, 2022,
                  Proceedings, Part {I}},
  optbooktitle = {{TACAS} 2022},
  series =	 {Lecture Notes in Computer Science},
  volume =	 13243,
  pages =	 {415--442},
  publisher =	 {Springer},
  address = {Cham},
  year =	 2022,
  opturl =		 {https://doi.org/10.1007/978-3-030-99524-9_24},
  doi =		 {10.1007/978-3-030-99524-9_24},
  timestamp =	 {Fri, 29 Apr 2022 14:50:36 +0200},
  biburl =
                  {https://dblp.org/rec/conf/tacas/BarbosaBBKLMMMN22.bib},
  bibsource =	 {dblp computer science bibliography,
                  https://dblp.org}
}

@article{Ehoh,
  author =	 {Petar Vukmirovic and Jasmin Blanchette and Simon
                  Cruanes and Stephan Schulz},
  title =	 {Extending a brainiac prover to lambda-free
                  higher-order logic},
  journal =	 {International Journal on Software Tools for Technology Transfer},
  volume =	 24,
  number =	 1,
  pages =	 {67--87},
  year =	 2022,
  opturl =		 {https://doi.org/10.1007/s10009-021-00639-7},
  doi =		 {10.1007/s10009-021-00639-7},
  timestamp =	 {Fri, 13 May 2022 19:53:01 +0200},
  biburl =
                  {https://dblp.org/rec/journals/sttt/VukmirovicBCS22.bib},
  bibsource =	 {dblp computer science bibliography,
                  https://dblp.org}
}

@article{Zipperpin,
  author =	 {Alexander Bentkamp and Jasmin Blanchette and Sophie
                  Tourret and Petar Vukmirovic and Uwe Waldmann},
  title =	 {Superposition with Lambdas},
  journal =	 {Journal of Automated Reasoning},
  volume =	 65,
  number =	 7,
  pages =	 {893--940},
  year =	 2021,
  opturl =		 {https://doi.org/10.1007/s10817-021-09595-y},
  doi =		 {10.1007/s10817-021-09595-y},
  timestamp =	 {Mon, 03 Jan 2022 22:07:16 +0100},
  biburl =
                  {https://dblp.org/rec/journals/jar/BentkampBTVW21.bib},
  bibsource =	 {dblp computer science bibliography,
                  https://dblp.org}
}

@article{TPTP,
  author =	 {Geoff Sutcliffe},
  title =	 {The {TPTP} Problem Library and Associated
                  Infrastructure - From {CNF} to {TH0}, {TPTP} v6.4.0},
  journal =	 {Journal of Automated Reasoning},
  volume =	 59,
  number =	 4,
  pages =	 {483--502},
  year =	 2017,
  url =		 {https://doi.org/10.1007/s10817-017-9407-7},
  doi =		 {10.1007/s10817-017-9407-7},
  timestamp =	 {Wed, 02 Sep 2020 13:30:01 +0200},
  biburl =	 {https://dblp.org/rec/journals/jar/Sutcliffe17.bib},
  bibsource =	 {dblp computer science bibliography,
                  https://dblp.org}
}

@InCollection{SEP,
  author =	 {Benzm{\"u}ller, Christoph and Andrews, Peter},
  title =	 {Church's Type Theory},
  booktitle =	 {The Stanford Encyclopedia of Philosophy},
  editor =	 {Edward N. Zalta},
  year =	 2019,
  edition =	 {Summer 2019},
  pages =	 {1--62 (in pdf version)},
  publisher =	 {Metaphysics Research Lab, Stanford University},
  address = {CA, USA},
  OPTurl = {https://plato.stanford.edu/entries/type-theory-church/},
  note = {\href{https://plato.stanford.edu/entries/type-theory-church/}{https://plato.stanford.edu/entries/type-theory-church/}}
}

@article{PrimSubst,
  Author =	 {Christoph Benzm{\"u}ller},
  Doi =		 {10.1023/A:1020840027781},
  Issn =	 {0039-7857},
  Journal =	 {Synthese},
  Keywords =	 {own, LEO Prover, Automated Reasoning, Higher Order
                  Logic, Henkin Semantics, ERIH PLUS, History of
                  Logic},
  Number =	 {1-2},
  Pages =	 {203-235},
  Title =	 {Comparing Approaches to Resolution based
                  Higher-Order Theorem Proving},
  url_preprint = {http://christoph-benzmueller.de/papers/J5.pdf},
  Volume =	 133,
  Year =	 2002,
}

@article{Andrews89,
  author =	 {Peter B. Andrews},
  title =	 {On Connections and Higher-Order Logic},
  journal =	 {Journal of Automated Reasoning},
  volume =	 5,
  number =	 3,
  pages =	 {257--291},
  year =	 1989,
  opturl =		 {https://doi.org/10.1007/BF00248320},
  doi =		 {10.1007/BF00248320},
  timestamp =	 {Wed, 02 Sep 2020 13:30:04 +0200},
  biburl =	 {https://dblp.org/rec/journals/jar/Andrews89.bib},
  bibsource =	 {dblp computer science bibliography,
                  https://dblp.org}
}

@inproceedings{Critique,
  author =	 {Alan Bundy},
  editor =	 {Antonis C. Kakas and Fariba Sadri},
  title =	 {A Critique of Proof Planning},
  booktitle =	 {Computational Logic: Logic Programming and Beyond,
                  Essays in Honour of {Robert} {A.} {Kowalski}, Part {II}},
  series =	 {Lecture Notes in Computer Science},
  volume =	 2408,
  pages =	 {160--177},
  publisher =	 {Springer},
  address = {Berlin, Heidelberg},
  year =	 2002,
  opturl =		 {https://doi.org/10.1007/3-540-45632-5_7},
  doi =		 {10.1007/3-540-45632-5_7},
  timestamp =	 {Tue, 14 May 2019 10:00:52 +0200},
  biburl =	 {https://dblp.org/rec/conf/birthday/Bundy02.bib},
  bibsource =	 {dblp computer science bibliography,
                  https://dblp.org}
}

@inproceedings{FreshStart,
  Address =	 {Siena, Italy},
  Author =	 {Christoph Benzm{\"u}ller and Andreas Meier and Erica
                  Melis and Martin Pollet and Volker Sorge},
  Booktitle =	 {Proceedings of the {IJCAR} 2001 Workshop: Future
                  Directions in Automated Reasoning},
  Pages =	 {25-37},
  Title =	 {Proof Planning: A Fresh Start?},
  url_preprint = {http://christoph-benzmueller.de/papers/W12.pdf},
  Year =	 2001,
  note = {\href{https://www.researchgate.net/publication/319393675}{https://www.researchgate.net/publication/319393675}},
}

@inproceedings{LemmaDiscovery,
  author =	 {Moa Johansson},
  editor =	 {Cezary Kaliszyk and Edwin C. Brady and Andrea
                  Kohlhase and Claudio Sacerdoti Coen},
  title =	 {Lemma Discovery for Induction - {A} Survey},
  booktitle = {Intelligent Computer Mathematics - 12th
                  International Conference, {CICM} 2019, Prague, Czech
                  Republic, July 8-12, 2019, Proceedings},
  optbooktitle =    {{CICM} 2019},		  
  series =	 {Lecture Notes in Computer Science},
  volume =	 11617,
  pages =	 {125--139},
  publisher =	 {Springer},
  address = {Cham},
  year =	 2019,
  opturl =		 {https://doi.org/10.1007/978-3-030-23250-4_9},
  doi =		 {10.1007/978-3-030-23250-4_9},
  timestamp =	 {Sun, 21 Jun 2020 17:42:36 +0200},
  biburl =	 {https://dblp.org/rec/conf/mkm/Johansson19.bib},
  bibsource =	 {dblp computer science bibliography,
                  https://dblp.org}
}

@article{Church40,
  author =	 {Alonzo Church},
  title =	 {A Formulation of the Simple Theory of Types},
  journal =	 {Journal of Symbolic Logic},
  volume =	 5,
  number =	 2,
  pages =	 {56--68},
  year =	 1940,
  url =		 {https://doi.org/10.2307/2266170},
  doi =		 {10.2307/2266170},
  timestamp =	 {Wed, 14 Nov 2018 10:49:18 +0100},
  biburl =	 {https://dblp.org/rec/journals/jsyml/Church40.bib},
  bibsource =	 {dblp computer science bibliography,
                  https://dblp.org}
}

@article{Leo2,
  Author =	 {Christoph Benzm{\"u}ller and Nik Sultana and
                  Paulson, Lawrence C. and Frank Theiss},
  Doi =		 {10.1007/s10817-015-9348-y},
  Journal =	 {Journal of Automated Reasoning},
  publisher =	 {Springer Netherlands},
  Keywords =	 {own, Automated Reasoning, Interactive Proof,
                  Ontology Reasoning, LEO Prover, Higher Order Logic,
                  DFG-2501-Selected},
  Number =	 4,
  Pages =	 {389-404},
  Title =	 {The Higher-Order Prover {LEO-II}},
  url_preprint = {https://www.researchgate.net/publication/280986731},
  Volume =	 55,
  Year =	 2015,
}

@inproceedings{cvc4,
  author    = {Clark W. Barrett and
               Christopher L. Conway and
               Morgan Deters and
               Liana Hadarean and
               Dejan Jovanovic and
               Tim King and
               Andrew Reynolds and
               Cesare Tinelli},
  editor    = {Ganesh Gopalakrishnan and
               Shaz Qadeer},
  title     = {{CVC4}},
  booktitle = {Computer Aided Verification - 23rd International Conference, {CAV}
               2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {6806},
  pages     = {171--177},
  publisher = {Springer},
  year      = {2011},
  url       = {https://doi.org/10.1007/978-3-642-22110-1\_14},
  doi       = {10.1007/978-3-642-22110-1\_14},
  timestamp = {Tue, 27 Jul 2021 08:54:13 +0200},
  biburl    = {https://dblp.org/rec/conf/cav/BarrettCDHJKRT11.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
