@inproceedings{mono-trans,
  author       = {Jasmin Christian Blanchette and
                  Sascha B{\"{o}}hme and
                  Andrei Popescu and
                  Nicholas Smallbone},
  editor       = {Nir Piterman and
                  Scott A. Smolka},
  title        = {Encoding Monomorphic and Polymorphic Types},
  booktitle    = {{TACAS} 2013},
  series       = {LNCS},
  volume       = {7795},
  pages        = {493--507},
  publisher    = {Springer},
  year         = {2013},
  XXXurl          = {https://doi.org/10.1007/978-3-642-36742-7\_34},
  XXXdoi          = {10.1007/978-3-642-36742-7\_34},
}


@inproceedings{smt-lib-mono,
  title={Extending {SMT-LIB} v2 with $\lambda$-Terms and Polymorphism},
  author={Richard Bonichon and David D{\'e}harbe and Cl{\'a}udia Tavares},
  editor       = {Philipp R{\"{u}}mmer and
                  Christoph M. Wintersteiger},
  booktitle = "SMT 2014",
  XXXbooktitle    = {Proceedings of the 12th International Workshop on Satisfiability Modulo
                  Theories, {SMT} 2014, affiliated with the 26th International Conference
                  on Computer Aided Verification {(CAV} 2014), the 7th International
                  Joint Conference on Automated Reasoning {(IJCAR} 2014), and the 17th
                  International Conference on Theory and Applications of Satisfiability
                  Testing {(SAT} 2014), Vienna, Austria, July 17-18, 2014},
  series       = {{CEUR} Workshop Proceedings},
  volume       = {1163},
  pages        = {53--62},
  publisher    = {CEUR-WS.org},
  year         = {2014},
  XXXurl          = {https://ceur-ws.org/Vol-1163/paper-08.pdf},
  timestamp    = {Fri, 10 Mar 2023 16:22:48 +0100},
  biburl       = {https://dblp.org/rec/conf/smt/BonichonDT14.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{expr-poly-types,
  author       = {Fran{\c{c}}ois Bobot and
                  Andrey Paskevich},
  editor       = {Cesare Tinelli and
                  Viorica Sofronie{-}Stokkermans},
  title        = {Expressing Polymorphic Types in a Many-Sorted Language},
  booktitle    = {FroCoS 2011},
  series       = {LNCS},
  volume       = {6989},
  pages        = {87--102},
  publisher    = {Springer},
  year         = {2011},
  XXXurl          = {https://doi.org/10.1007/978-3-642-24364-6\_7},
  XXXdoi          = {10.1007/978-3-642-24364-6\_7},
}


@phdthesis{sb-phd,
  type = "Ph{D} thesis",
  author       = {Sascha B{\"{o}}hme},
  title        = {Proving Theorems of Higher-Order Logic with {SMT} Solvers},
  school       = {Technische Universität München},
  year         = {2012},
  XXXurl          = {https://nbn-resolving.org/urn:nbn:de:bvb:91-diss-20120511-1084525-1-4},
  XXXurn          = {urn:nbn:de:bvb:91-diss-20120511-1084525-1-4},
}

@article{vamp,
  author       = {Alexandre Riazanov and
                  Andrei Voronkov},
  title        = {The design and implementation of {VAMPIRE}},
  journal      = {{AI} Commun.},
  volume       = {15},
  number       = {2--3},
  pages        = {91--110},
  year         = {2002},
  XXXurl          = {http://content.iospress.com/articles/ai-communications/aic259},
}

@inproceedings{judgement,
  author       = {Sascha B{\"{o}}hme and
                  Tobias Nipkow},
  editor       = {J{\"{u}}rgen Giesl and
                  Reiner H{\"{a}}hnle},
  title        = {Sledgehammer: Judgement {D}ay},
  booktitle    = {{IJCAR} 2010},
  series       = {LNCS},
  volume       = {6173},
  pages        = {107--121},
  publisher    = {Springer},
  year         = {2010},
  XXXurl          = {https://doi.org/10.1007/978-3-642-14203-1\_9},
  XXXdoi          = {10.1007/978-3-642-14203-1\_9},
}

@article{zipp,
  author       = {Alexander Bentkamp and
                  Jasmin Blanchette and
                  Simon Cruanes and
                  Uwe Waldmann},
  title        = {Superposition for Lambda-Free Higher-Order Logic},
  journal      = {Log. Methods Comput. Sci.},
  volume       = {17},
  number       = {2},
  year         = {2021},
  XXXurl          = {https://lmcs.episciences.org/7349},
}

@article{e,
  author       = {Stephan Schulz},
  title        = {E -- A brainiac theorem prover},
  journal      = {{AI} Commun.},
  volume       = {15},
  number       = {2--3},
  pages        = {111--126},
  year         = {2002},
  XXXurl          = {http://content.iospress.com/articles/ai-communications/aic260},
}

@article{tptp,

  author       = {Geoff Sutcliffe},
  title        = {The {TPTP} Problem Library and Associated Infrastructure -- From {CNF}
                  to {TH0}, {TPTP} v8.2.0},
  journal      = {J. Autom. Reason.},
  volume       = {59},
  number       = {4},
  pages        = {483--502},
  year         = {2017},
  XXXurl          = {https://doi.org/10.1007/s10817-017-9407-7},
  XXXdoi          = {10.1007/S10817-017-9407-7},
}

@inproceedings{leo-iii,
  author       = {Alexander Steen and
                  Christoph Benzm{\"{u}}ller},
  editor       = {Giuseppe De Giacomo and
                  Alejandro Catal{\'{a}} and
                  Bistra Dilkina and
                  Michela Milano and
                  Sen{\'{e}}n Barro and
                  Alberto Bugar{\'{\i}}n and
                  J{\'{e}}r{\^{o}}me Lang},
  title        = {The Higher-Order Prover {Leo-III}},
  booktitle    = {{ECAI} 2020 - 24th European Conference on Artificial Intelligence,
                  29 August-8 September 2020, Santiago de Compostela, Spain, August
                  29 - September 8, 2020 - Including 10th Conference on Prestigious
                  Applications of Artificial Intelligence ({PAIS} 2020)},
  series       = {Frontiers in Artificial Intelligence and Applications},
  volume       = {325},
  pages        = {2937--2938},
  publisher    = {{IOS} Press},
  year         = {2020},
  XXXurl          = {https://doi.org/10.3233/FAIA200462},
  XXXdoi          = {10.3233/FAIA200462},
}

@inproceedings{th1,
  author       = {Cezary Kaliszyk and
                  Geoff Sutcliffe and
                  Florian Rabe},
  editor       = {Pascal Fontaine and
                  Stephan Schulz and
                  Josef Urban},
  title        = {{TH1}: The {TPTP} Typed Higher-Order Form with Rank-1 Polymorphism},
  booktitle    = {PAAR 2016},
  series       = {{CEUR} Workshop Proceedings},
  volume       = {1635},
  pages        = {41--55},
  publisher    = {CEUR-WS.org},
  year         = {2016},
  XXXurl          = {https://ceur-ws.org/Vol-1635/paper-05.pdf},
}

@inproceedings{slind-norrish-2008,
  author       = {Konrad Slind and
                  Michael Norrish},
  editor       = {Otmane A{\"{\i}}t Mohamed and
                  C{\'{e}}sar A. Mu{\~{n}}oz and
                  Sofi{\`{e}}ne Tahar},
  title        = {A Brief Overview of {HOL4}},
  booktitle    = {TPHOLs 2008},
  series       = {LNCS},
  volume       = {5170},
  pages        = {28--32},
  publisher    = {Springer},
  year         = {2008},
  XXXurl          = {https://doi.org/10.1007/978-3-540-71067-7\_6},
  XXXdoi          = {10.1007/978-3-540-71067-7\_6},
}

@inproceedings{harrison-2009,
  author       = {John Harrison},
  editor       = {Stefan Berghofer and
                  Tobias Nipkow and
                  Christian Urban and
                  Makarius Wenzel},
  title        = {{HOL} {L}ight: An Overview},
  booktitle    = {TPHOLs 2009},
  series       = {LNCS},
  volume       = {5674},
  pages        = {60--66},
  publisher    = {Springer},
  year         = {2009},
  XXXurl          = {https://doi.org/10.1007/978-3-642-03359-9\_4},
  XXXdoi          = {10.1007/978-3-642-03359-9\_4},
}

@book{nipkow-et-al-2002,
  author       = {Tobias Nipkow and
                  Lawrence C. Paulson and
                  Markus Wenzel},
  title        = {Isabelle/HOL: A Proof Assistant for Higher-Order Logic},
  series       = {LNCS},
  volume       = {2283},
  publisher    = {Springer},
  year         = {2002},
  XXXurl          = {https://doi.org/10.1007/3-540-45949-9},
  XXXdoi          = {10.1007/3-540-45949-9},
  XXXisbn         = {3-540-43376-7},
}

@inproceedings{bhayat-reger-2020,
  author       = {Ahmed Bhayat and
                  Giles Reger},
  editor       = {Nicolas Peltier and
                  Viorica Sofronie{-}Stokkermans},
  title        = {A Polymorphic {V}ampire (Short Paper)},
  booktitle    = {{IJCAR} 2020, Part {II}},
  series       = {LNCS},
  volume       = {12167},
  pages        = {361--368},
  publisher    = {Springer},
  year         = {2020},
  XXXurl          = {https://doi.org/10.1007/978-3-030-51054-1\_21},
  XXXdoi          = {10.1007/978-3-030-51054-1\_21},
}

@inproceedings{blanchette-paskevich-2013,
  author       = {Jasmin Christian Blanchette and
                  Andrei Paskevich},
  editor       = {Maria Paola Bonacina},
  title        = {{TFF1:} {T}he {TPTP} Typed First-Order Form with Rank-1 Polymorphism},
  booktitle    = {{CADE-24}},
  series       = {LNCS},
  volume       = {7898},
  pages        = {414--420},
  publisher    = {Springer},
  year         = {2013},
  XXXurl          = {https://doi.org/10.1007/978-3-642-38574-2\_29},
  XXXdoi          = {10.1007/978-3-642-38574-2\_29},
}


TODO

@manual{hammer,
  author      = {Jasmin Christian Blanchette and
                 Lawrence C. Paulson},
  title       = {Hammering Away: A User’s Guide to Sledgehammer for {Isabelle/HOL}},
  year        = {2019},
}

@inproceedings{harrison-1996,
  author       = {John Harrison},
  editor       = {Michael A. McRobbie and
                  John K. Slaney},
  title        = {Optimizing Proof Search in Model Elimination},
  booktitle    = {CADE-13},
  series       = {LNCS},
  volume       = {1104},
  pages        = {313--327},
  publisher    = {Springer},
  year         = {1996},
  XXXurl          = {https://doi.org/10.1007/3-540-61511-3\_97},
  XXXdoi          = {10.1007/3-540-61511-3\_97},
}

@inproceedings{hoder-voronkov-2011,
  author       = {Krystof Hoder and
                  Andrei Voronkov},
  editor       = {Nikolaj S. Bj{\o}rner and
                  Viorica Sofronie{-}Stokkermans},
  title        = {Sine Qua Non for Large Theory Reasoning},
  booktitle    = {{CADE-23}},
  series       = {LNCS},
  volume       = {6803},
  pages        = {299--314},
  publisher    = {Springer},
  year         = {2011},
  XXXurl          = {https://doi.org/10.1007/978-3-642-22438-6\_23},
  XXXdoi          = {10.1007/978-3-642-22438-6\_23},
  timestamp    = {Mon, 28 Aug 2023 21:17:45 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/HoderV11.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{meng-paulson-2009,
  author       = {Jia Meng and
                  Lawrence C. Paulson},
  title        = {Lightweight relevance filtering for machine-generated resolution problems},
  journal      = {J. Appl. Log.},
  volume       = {7},
  number       = {1},
  pages        = {41--57},
  year         = {2009},
  XXXurl          = {https://doi.org/10.1016/j.jal.2007.07.004},
  XXXdoi          = {10.1016/J.JAL.2007.07.004},
  timestamp    = {Tue, 28 May 2024 16:25:09 +0200},
  biburl       = {https://dblp.org/rec/journals/japll/MengP09.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{vukmirovic-et-al-2021,
  author    = {Petar Vukmirovi\'c and
               Alexander Bentkamp and
               Jasmin Blanchette and
               Simon Cruanes and
               Visa Nummelin and
               Sophie Tourret},
  editor    = {Andr{\'{e}} Platzer and
               Geoff Sutcliffe},
  title     = {Making higher-order superposition work},
  booktitle = {{CADE}-28},
  series    = {LNCS},
  volume    = {12699},
  pages     = {415--432},
  publisher = {Springer},
  year      = {2021},
  XXXurl       = {https://doi.org/10.1007/978-3-030-79876-5\_24},
  XXXdoi       = {10.1007/978-3-030-79876-5\_24},
}

@inproceedings{paulson-blanchette-2010,
  author = "Lawrence C. Paulson and Jasmin Christian Blanchette",
  title = "Three Years of Experience with {Sledgehammer}, a~Practical Link Between Automatic and Interactive Theorem Provers",
  booktitle = "{IWIL-2010}",
  editor    = {Geoff Sutcliffe and Stephan Schulz and Eugenia Ternovska},
  series    = {EPiC},
  volume    = {2},
  pages     = {1--11},
  year      = {2012},
  publisher = {EasyChair}
}