@inproceedings(GandalfFOL,
 author       = {Andreas Abel and Thierry Coquand and Ulf Norell},
 year         = {2005},
 title        = {Connecting a Logical Framework to a First-Order Logic Prover},
 editor       = {Bernhard Gramlich},
 booktitle    = {Frontiers of Combining Systems (FroCoS 2005)},
 series       = {LNCS},
 volume       = {3717},
 publisher    = {Springer},
 pages        = {285--301},
 doi          = {10.1007/11559306\_17},
)
@inproceedings(f_star,
 author       = {Alejandro Aguirre and Hri\begingroup\let \relax\relax \endgroup[Please insert \PrerenderUnicode{\unichar{539}} into preamble]cu, C{\u{a}}t{\u{a}}lin and Chantal Keller and Nikhil Swamy},
 year         = {2016},
 title        = {From $\mathrm{F}^*$ to {SMT} (Extended Abstract)},
 booktitle    = {Hammers for Type Theories, HaTT 2016},
 note         = {To appear},
)
@inproceedings(smtcoq,
 author       = {Micha{\"{e}}l Armand and Germain Faure and Benjamin Gr{\'{e}}goire and Chantal Keller and Laurent Th{\'{e}}ry and Benjamin Werner},
 year         = {2011},
 title        = {A Modular Integration of {SAT/SMT} Solvers to {C}oq through Proof Witnesses},
 editor       = {Jean{-}Pierre Jouannaud and Zhong Shao},
 booktitle    = {Certified Programs and Proofs (CPP 2011)},
 series       = {LNCS},
 volume       = {7086},
 publisher    = {Springer},
 pages        = {135--150},
 doi          = {10.1007/978-3-642-25379-9\_12},
)
@article(Matita14,
 author       = {Andrea Asperti and Wilmer Ricciotti and {Sacerdoti Coen}, Claudio},
 year         = {2014},
 title        = {Matita Tutorial},
 journal      = {J. Formalized Reasoning},
 volume       = {7},
 number       = {2},
 pages        = {91--199},
 doi          = {10.6092/issn.1972-5787/4651},
)
@inproceedings(DBLP:conf/mkm/AspertiT07,
 author       = {Andrea Asperti and Enrico Tassi},
 year         = {2007},
 title        = {Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case},
 editor       = {Manuel Kauers and Manfred Kerber and Robert Miner and Wolfgang Windsteiger},
 booktitle    = {Mathematical Knowledge Management (MKM 2007)},
 series       = {LNCS},
 volume       = {4573},
 publisher    = {Springer},
 pages        = {146--160},
 doi          = {10.1007/978-3-540-73086-6\_14},
)
@article(Bancerek03,
 author       = {Grzegorz Bancerek},
 year         = {2003},
 title        = {On the structure of Mizar types},
 journal      = {Electr. Notes Theor. Comput. Sci.},
 volume       = {85},
 number       = {7},
 pages        = {69--85},
 doi          = {10.1016/S1571-0661(04)80758-8},
)
@inproceedings(Bancerek15,
 author       = {Grzegorz Bancerek and Czeslaw Bylinski and Adam Grabowski and Artur Kornilowicz and Roman Matuszewski and Adam Naumowicz and Karol Pak and Josef Urban},
 year         = {2015},
 title        = {Mizar: State-of-the-art and Beyond},
 booktitle    = {Intelligent Computer Mathematics - International Conference, {CICM} 2015, Washington, DC, USA, July 13-17, 2015, Proceedings},
 pages        = {261--279},
 doi          = {10.1007/978-3-319-20615-8\_17},
)
@inproceedings(Bertot08Coq,
 author       = {Yves Bertot},
 year         = {2008},
 title        = {A Short Presentation of {C}oq},
 editor       = {Otmane A{\"{\i}}t Mohamed and Mu{\~{n}}oz, C{\'{e}}sar A. and Sofi{\`{e}}ne Tahar},
 booktitle    = {Theorem Proving in Higher Order Logics (TPHOLs 2008)},
 series       = {LNCS},
 volume       = {5170},
 publisher    = {Springer},
 pages        = {12--16},
 doi          = {10.1007/978-3-540-71067-7\_3},
)
@article(BezemHendriksNivelle2002,
 author       = {Marc Bezem and Dimitri Hendriks and Hans de Nivelle},
 year         = {2002},
 title        = {Automated Proof Construction in Type Theory Using Resolution},
 journal      = {J. Autom. Reasoning},
 volume       = {29},
 number       = {3-4},
 pages        = {253--275},
 doi          = {10.1023/A:1021939521172},
)
@article(jbcklpju-h4qed-jfr,
 author       = {Jasmin C. Blanchette and Cezary Kaliszyk and Lawrence C. Paulson and Josef Urban},
 year         = {2016},
 title        = {Hammering towards {QED}},
 journal      = {J. Formalized Reasoning},
 volume       = {9},
 number       = {1},
 pages        = {101--148},
 doi          = {10.6092/issn.1972-5787/4593},
 url          = {http://jfr.unibo.it/article/view/4593},
)
@unpublished(mash2,
 author       = {Jasmin Christian Blanchette and David Greenaway and Cezary Kaliszyk and K\begingroup\let \relax\relax \endgroup[Pleaseinsert\PrerenderUnicode{ü}intopreamble]hlwein, Daniel and Josef Urban},
 year         = {2016},
 title        = {A Learning-Based Relevance Filter for {Isabelle/HOL}},
 note         = {J.~Autom. Reasoning, to appear. \url{http://cl-informatik.uibk.ac.at/cek/mash2.pdf}},
)
@inproceedings(BoveDN09Agda,
 author       = {Ana Bove and Peter Dybjer and Ulf Norell},
 year         = {2009},
 title        = {A Brief Overview of {A}gda - {A} Functional Language with Dependent Types},
 editor       = {Stefan Berghofer and Tobias Nipkow and Christian Urban and Makarius Wenzel},
 booktitle    = {Theorem Proving in Higher Order Logics (TPHOLs 2009)},
 series       = {LNCS},
 volume       = {5674},
 publisher    = {Springer},
 pages        = {73--78},
 doi          = {10.1007/978-3-642-03359-9\_6},
)
@inproceedings(Corbineau03,
 author       = {Pierre Corbineau},
 year         = {2003},
 title        = {First-Order Reasoning in the Calculus of Inductive Constructions},
 editor       = {Stefano Berardi and Mario Coppo and Ferruccio Damiani},
 booktitle    = {Types for Proofs and Programs (TYPES 2003)},
 series       = {LNCS},
 volume       = {3085},
 publisher    = {Springer},
 pages        = {162--177},
 doi          = {10.1007/978-3-540-24849-1\_11},
)
@article(Dyckhoff1992,
 author       = {Roy Dyckhoff},
 year         = {1992},
 title        = {Contraction-Free Sequent Calculi for Intuitionistic Logic},
 journal      = {J. Symb. Log.},
 volume       = {57},
 number       = {3},
 pages        = {795--807},
 doi          = {10.2307/2275431},
)
@inproceedings(onelogictorule,
 author       = {Jean-Christophe Filli{\^{a}}tre},
 year         = {2013},
 title        = {One Logic to Use Them All},
 editor       = {Maria Paola Bonacina},
 booktitle    = {International Conference on Automated Deduction (CADE 2013)},
 series       = {LNCS},
 volume       = {7898},
 publisher    = {Springer},
 pages        = {1--20},
 doi          = {10.1007/978-3-642-38574-2\_1},
)
@inproceedings(FilliatreP13,
 author       = {Jean-Christophe Filli{\^{a}}tre and Andrei Paskevich},
 year         = {2013},
 title        = {Why3 - Where Programs Meet Provers},
 booktitle    = {European Symposium on Programming (ESOP 2013)},
 pages        = {125--128},
 doi          = {10.1007/978-3-642-37036-6\_8},
)
@article(Hales-Developments,
 author       = {Thomas Hales},
 year         = {2013--2014},
 title        = {Developments in Formal Proofs},
 journal      = {S\begingroup\let \relax\relax \endgroup[Pleaseinsert\PrerenderUnicode{é}intopreamble]minaire Bourbaki},
 volume       = {1086},
 note         = {\href{http://arxiv.org/abs/1408.6474}{abs/1408.6474}},
)
@inproceedings(harrison-2009,
 author       = {John Harrison},
 year         = {2009},
 title        = {{HOL Light}: An Overview},
 editor       = {Stefan Berghofer and Tobias Nipkow and Christian Urban and Makarius Wenzel},
 booktitle    = {Theorem Proving in Higher Order Logics (TPHOLs 2009)},
 series       = {LNCS},
 volume       = {5674},
 publisher    = {Springer},
 pages        = {60--66},
 doi          = {10.1007/978-3-642-03359-9\_4},
)
@inproceedings(hurd2003d,
 author       = {Joe Hurd},
 year         = {2003},
 title        = {First-Order Proof Tactics in Higher-Order Logic Theorem Provers},
 editor       = {Myla Archer and Ben Di Vito and Mu{\~{n}}oz, C{\'{e}}sar},
 booktitle    = {Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003)},
 series       = {{NASA} Technical Reports},
 volume       = {NASA/CP-2003-212448},
 pages        = {56--68},
 url          = {http://techreports.larc.nasa.gov/ltrs/PDF/2003/cp/NASA-2003-cp212448.pdf},
)
@article(holyhammer,
 author       = {Cezary Kaliszyk and Josef Urban},
 year         = {2014},
 title        = {Learning-Assisted Automated Reasoning with {F}lyspeck},
 journal      = {J. Autom. Reasoning},
 volume       = {53},
 number       = {2},
 pages        = {173--213},
 doi          = {10.1007/s10817-014-9303-3},
)
@article(ckjumiz40,
 author       = {Cezary Kaliszyk and Josef Urban},
 year         = {2015},
 title        = {{MizAR} 40 for {M}izar 40},
 journal      = {J. Autom. Reasoning},
 volume       = {55},
 number       = {3},
 pages        = {245--256},
 doi          = {10.1007/s10817-015-9330-8},
)
@inproceedings(Vampire,
 author       = {Laura Kov{\'a}cs and Andrei Voronkov},
 year         = {2013},
 title        = {First-Order Theorem Proving and {V}ampire},
 booktitle    = {Computer-Aided Verification (CAV 2013)},
 pages        = {1--35},
 doi          = {10.1007/978-3-642-39799-8\_1},
)
@article(MengPaulson2008,
 author       = {Jia Meng and Lawrence C. Paulson},
 year         = {2008},
 title        = {Translating Higher-Order Clauses to First-Order Clauses},
 journal      = {Journal of Automated Reasoning},
 volume       = {40},
 number       = {1},
 pages        = {35--60},
 doi          = {10.1007/s10817-007-9085-y},
)
@inproceedings(MouraSelsam2016,
 author       = {Leonardo de Moura and Daniel Selsam},
 year         = {2016},
 title        = {Congruence Closure in Intensional Type Theory},
 booktitle    = {International Joint Conference on Automated Reasoning, IJCAR 2016},
 note         = {To appear},
)
@inproceedings(MouraKADR15Lean,
 author       = {Leonardo Mendon{\c{c}}a de Moura and Soonho Kong and Jeremy Avigad and Floris van Doorn and Jakob von Raumer},
 year         = {2005},
 title        = {The {L}ean Theorem Prover},
 editor       = {Amy P. Felty and Aart Middeldorp},
 booktitle    = {International Conference on Automated Deduction (CADE 2005)},
 series       = {LNCS},
 volume       = {9195},
 publisher    = {Springer},
 pages        = {378--388},
 doi          = {10.1007/978-3-319-21401-6\_26},
)
@inproceedings(de-moura-bjoerner-2008,
 author       = {Leonardo Mendon\c{c}a de Moura and Bj{\o}rner, Nikolaj},
 year         = {2008},
 title        = {{Z3}: {An} Efficient {SMT} Solver},
 editor       = {C. R. Ramakrishnan and Jakob Rehof},
 booktitle    = {TACAS 2008},
 series       = {LNCS},
 volume       = {4963},
 publisher    = {Springer},
 pages        = {337--340},
 doi          = {10.1007/978-3-540-78800-3\_24},
)
@inproceedings(sledgehammer10,
 author       = {Lawrence C. Paulson and Jasmin Blanchette},
 year         = {2010},
 title        = {Three Years of Experience with {S}ledgehammer, a Practical Link between Automated and Interactive Theorem Provers},
 booktitle    = {8th IWIL},
 url          = {http://www4.in.tum.de/~schulz/PAPERS/STS-IWIL-2010.pdf},
)
@inproceedings(DBLP:conf/cade/SchmittLKN01,
 author       = {Stephan Schmitt and Lori Lorigo and Christoph Kreitz and Aleksey Nogin},
 year         = {2001},
 title        = {JProver : Integrating Connection-Based Theorem Proving into Interactive Proof Assistants},
 editor       = {Rajeev Gor{\'{e}} and Alexander Leitsch and Tobias Nipkow},
 booktitle    = {Automated Reasoning, First International Joint Conference, {IJCAR} 2001, Siena, Italy, June 18-23, 2001, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {2083},
 publisher    = {Springer},
 pages        = {421--426},
 doi          = {10.1007/3-540-45744-5\_34},
)
@inproceedings(urzy1,
 author       = {Aleksy Schubert and Pawe{\l} Urzyczyn and Konrad Zdanowski},
 year         = {2015},
 title        = {On the {M}ints Hierarchy in First-Order Intuitionistic Logic},
 editor       = {Andrew M. Pitts},
 booktitle    = {Foundations of Software Science and Computation Structures (FoSSaCS 2015)},
 series       = {Lecture Notes in Computer Science},
 volume       = {9034},
 publisher    = {Springer},
 pages        = {451--465},
 doi          = {10.1007/978-3-662-46678-0\_29},
)
@inproceedings(Schulz13,
 author       = {Stephan Schulz},
 year         = {2013},
 title        = {System Description: {E} 1.8},
 booktitle    = {Logic for Programming, Artificial Intelligence (LPAR 2013)},
 pages        = {735--743},
 doi          = {10.1007/978-3-642-45221-5\_49},
)
@inproceedings(slind-norrish-2008,
 author       = {Konrad Slind and Michael Norrish},
 year         = {2008},
 title        = {A Brief Overview of {HOL4}},
 editor       = {Otmane Ait Mohamed and Mu{\~n}oz, C\'esar and Sofi\`ene Tahar},
 booktitle    = {TPHOLs~2008},
 series       = {{LNCS}},
 volume       = {5170},
 publisher    = {Springer},
 pages        = {28--32},
 doi          = {10.1007/978-3-540-71067-7\_6},
)
@article(optimizedencod,
 author       = {Tanel Tammet and Jan M. Smith},
 year         = {1998},
 title        = {Optimized Encodings of Fragments of Type Theory in First-Order Logic},
 journal      = {J. Log. Comput.},
 volume       = {8},
 number       = {6},
 pages        = {713--744},
 doi          = {10.1093/logcom/8.6.713},
)
@inproceedings(WenzelPN08,
 author       = {Makarius Wenzel and Lawrence C. Paulson and Tobias Nipkow},
 year         = {2008},
 title        = {The {I}sabelle Framework},
 editor       = {Otmane A\"{\i}t Mohamed and Mu{\~n}oz, C{\'e}sar A. and Sofi{\`e}ne Tahar},
 booktitle    = {Theorem Proving in Higher Order Logics (TPHOLs 2008)},
 series       = {LNCS},
 volume       = {5170},
 publisher    = {Springer},
 pages        = {33--38},
 doi          = {10.1007/978-3-540-71067-7\_7},
)
@inproceedings(Wiedijk2007,
 author       = {Freek Wiedijk},
 year         = {2007},
 title        = {Mizar's Soft Type System},
 booktitle    = {Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings},
 pages        = {383--399},
 doi          = {10.1007/978-3-540-74591-4\_28},
)