@article(abs-1108-3446,
 author       = "Jesse Alama and Tom Heskes and Daniel K\"{u}hlwein and Evgeni Tsivtsivadze and Josef Urban",
 year         = "2014",
 title        = "Premise Selection for Mathematics by Corpus Analysis and Kernel Methods",
 journal      = "J. Autom. Reasoning",
 volume       = "52",
 number       = "2",
 pages        = "191--213",
 doi          = "10.1007/s10817-013-9286-5",
)
@inproceedings(BlanchetteBPS13,
 author       = "Jasmin Christian Blanchette and Sascha B{\"o}hme and Andrei Popescu and Nicholas Smallbone",
 year         = "2013",
 title        = "Encoding Monomorphic and Polymorphic Types",
 editor       = "Nir Piterman and Scott A. Smolka",
 booktitle    = "TACAS",
 series       = "Lecture Notes in Computer Science",
 volume       = "7795",
 publisher    = "Springer",
 pages        = "493--507",
 url          = "http://dx.doi.org/10.1007/978-3-642-36742-7_34",
)
@article(mizar-in-a-nutshell,
 author       = "Adam Grabowski and Artur Korni{\l }owicz and Adam Naumowicz",
 year         = "2010",
 title        = "{M}izar in a Nutshell",
 journal      = "Journal of Formalized Reasoning",
 volume       = "3",
 number       = "2",
 pages        = "153--245",
)
@inproceedings(Hales05,
 author       = "Thomas C. Hales",
 year         = "2006",
 title        = "Introduction to the {F}lyspeck Project",
 editor       = "Thierry Coquand and Henri Lombardi and Marie-Fran{\c {c}}oise Roy",
 booktitle    = "Mathematics, Algorithms, Proofs",
 series       = "Dagstuhl Seminar Proceedings",
 volume       = "05021",
 publisher    = "Internationales Begegnungs- und Forschungszentrum f{\"u}r Informatik (IBFI), Schloss Dagstuhl, Germany",
 address      = "Dagstuhl, Germany",
 pages        = "1--11",
 url          = "http://drops.dagstuhl.de/opus/volltexte/2006/432",
)
@inproceedings(Harrison96,
 author       = "John Harrison",
 year         = "1996",
 title        = "{HOL Light}: A Tutorial Introduction",
 editor       = "Mandayam K. Srivas and Albert John Camilleri",
 booktitle    = "FMCAD",
 series       = "LNCS",
 volume       = "1166",
 publisher    = "Springer",
 pages        = "265--269",
 url          = "http://dx.doi.org/10.1007/BFb0031814",
)
@inproceedings(HoderV11,
 author       = "Krystof Hoder and Andrei Voronkov",
 year         = "2011",
 title        = "Sine Qua Non for Large Theory Reasoning",
 editor       = "Nikolaj Bj{\o }rner and Viorica Sofronie-Stokkermans",
 booktitle    = "CADE",
 series       = "LNCS",
 volume       = "6803",
 publisher    = "Springer",
 pages        = "299--314",
 url          = "http://dx.doi.org/10.1007/978-3-642-22438-6_23",
)
@article(hhmcs,
 author       = "Cezary Kaliszyk and Josef Urban",
 year         = "2013",
 title        = "{HOL(y)Hammer}: Online {ATP} Service for {HOL Light}",
 journal      = "CoRR",
 volume       = "abs/1309.4962",
 url          = "http://arxiv.org/abs/1309.4962",
 note         = "Accepted for publication in Mathematics in Computer Science",
)
@article(KaliszykU13b,
 author       = "Cezary Kaliszyk and Josef Urban",
 year         = "2013",
 title        = "{MizAR 40 for Mizar 40}",
 journal      = "CoRR",
 volume       = "abs/1310.2805",
 url          = "http://arxiv.org/abs/1310.2805",
)
@inproceedings(EasyChair:74,
 author       = "Cezary Kaliszyk and Josef Urban",
 year         = "2013",
 title        = "Stronger Automation for {F}lyspeck by Feature Weighting and Strategy Evolution",
 editor       = "Jasmin Christian Blanchette and Josef Urban",
 booktitle    = "PxTP 2013",
 series       = "EPiC Series",
 volume       = "14",
 publisher    = "EasyChair",
 pages        = "87--95",
)
@article(holyhammer,
 author       = "Cezary Kaliszyk and Josef Urban",
 year         = "2014",
 title        = "Learning-assisted Automated Reasoning with {F}lyspeck",
 journal      = "Journal of Automated Reasoning",
 doi          = "10.1007/s10817-014-9303-3",
 note         = "\url {http://dx.doi.org/10.1007/s10817-014-9303-3}",
)
@article(malar14,
 author       = "Cezary Kaliszyk and Josef Urban and Ji\v {r}\'i Vysko\v {c}il",
 year         = "2014",
 title        = "Machine Learner for Automated Reasoning 0.4 and 0.5",
 journal      = "CoRR",
 volume       = "abs/1402.2359",
 url          = "http://arxiv.org/abs/1402.2359",
 note         = "Accepted to PAAR'14",
)
@unpublished(kaufmann98_acl2,
 author       = "Matt Kaufmann and J Strother Moore",
 year         = "1998",
 title        = "A precise description of the {ACL2} logic",
 note         = "\url {http://www.cs.utexas.edu/users/moore/publications/km97a.pdf}",
)
@inproceedings(Vampire,
 author       = "Laura Kov{\'a}cs and Andrei Voronkov",
 year         = "2013",
 title        = "First-Order Theorem Proving and {V}ampire",
 editor       = "Natasha Sharygina and Helmut Veith",
 booktitle    = "CAV",
 series       = "Lecture Notes in Computer Science",
 volume       = "8044",
 publisher    = "Springer",
 pages        = "1--35",
 url          = "http://dx.doi.org/10.1007/978-3-642-39799-8_1",
)
@inproceedings(KuhlweinBKU13,
 author       = "Daniel K\"uhlwein and Jasmin Christian Blanchette and Cezary Kaliszyk and Josef Urban",
 year         = "2013",
 title        = "{MaSh}: Machine Learning for {Sledgehammer}",
 editor       = "Sandrine Blazy and Christine Paulin-Mohring and David Pichardie",
 booktitle    = "Proc. of the 4th International Conference on Interactive Theorem Proving (ITP'13)",
 series       = "LNCS",
 volume       = "7998",
 publisher    = "Springer",
 pages        = "35--50",
 doi          = "10.1007/978-3-642-39634-2_6",
 url          = "http://cl-informatik.uibk.ac.at/users/cek/docs/kuehlwein-itp13.pdf",
)
@inproceedings(KuhlweinLTUH12,
 author       = "Daniel K{\"u}hlwein and Twan van Laarhoven and Evgeni Tsivtsivadze and Josef Urban and Tom Heskes",
 year         = "2012",
 title        = "Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics",
 editor       = "Bernhard Gramlich and Dale Miller and Uli Sattler",
 booktitle    = "IJCAR",
 series       = "LNCS",
 volume       = "7364",
 publisher    = "Springer",
 pages        = "378--392",
 url          = "http://dx.doi.org/10.1007/978-3-642-31365-3_30",
)
@article(MengP08,
 author       = "Jia Meng and Lawrence C. Paulson",
 year         = "2008",
 title        = "Translating Higher-Order Clauses to First-Order Clauses",
 journal      = "J. Autom. Reasoning",
 volume       = "40",
 number       = "1",
 pages        = "35--60",
 url          = "http://dx.doi.org/10.1007/s10817-007-9085-y",
)
@article(MengP09,
 author       = "Jia Meng and Lawrence C. Paulson",
 year         = "2009",
 title        = "{Lightweight relevance filtering for machine-generated resolution problems}",
 journal      = "J. Applied Logic",
 volume       = "7",
 number       = "1",
 pages        = "41--57",
 url          = "http://dx.doi.org/10.1016/j.jal.2007.07.004",
)
@inproceedings(z3,
 author       = "Leonardo Mendon\c {c}a de Moura and Nikolaj Bj{\o }rner",
 year         = "2008",
 title        = "{Z3: An Efficient SMT Solver}",
 editor       = "C. R. Ramakrishnan and Jakob Rehof",
 booktitle    = "TACAS",
 series       = "LNCS",
 volume       = "4963",
 publisher    = "Springer",
 pages        = "337--340",
 url          = "http://dx.doi.org/10.1007/978-3-540-78800-3_24",
)
@inproceedings(NilesP01,
 author       = "Ian Niles and Adam Pease",
 year         = "2001",
 title        = "Towards a standard upper ontology",
 booktitle    = "FOIS",
 pages        = "2--9",
 url          = "http://doi.acm.org/10.1145/505168.505170",
)
@inproceedings(RRG05,
 author       = "D. Ramachandran and Reagan P. and K. Goolsbey",
 year         = "2005",
 title        = "{First-orderized {ResearchCyc}: Expressiveness and Efficiency in a Common Sense Knowledge Base}",
 editor       = "Shvaiko P.",
 booktitle    = "{Proceedings of the Workshop on Contexts and Ontologies: Theory, Practice and Applications}",
)
@article(Sch02-AICOMM,
 author       = "Stephan Schulz",
 year         = "2002",
 title        = "{E - A Brainiac Theorem Prover}",
 journal      = "AI Commun.",
 volume       = "15",
 number       = "2-3",
 pages        = "111--126",
 url          = "http://iospress.metapress.com/content/n908n94nmvk59v3c/",
)
@article(Sutcliffe13,
 author       = "Geoff Sutcliffe",
 year         = "2013",
 title        = "The 6th {IJCAR} automated theorem proving system competition - {CASC-J6}",
 journal      = "AI Commun.",
 volume       = "26",
 number       = "2",
 pages        = "211--223",
 url          = "http://dx.doi.org/10.3233/AIC-130550",
)
@article(Urb04-MPTP0,
 author       = "Josef Urban",
 year         = "2004",
 title        = "{MPTP - Motivation, Implementation, First Experiments}",
 journal      = "Journal of Automated Reasoning",
 volume       = "33",
 number       = "3-4",
 pages        = "319--339",
 doi          = "10.1007/s10817-004-6245-1",
)
@article(blistr,
 author       = "Josef Urban",
 year         = "2014",
 title        = "{BliStr: The Blind Strategymaker}",
 journal      = "CoRR",
 volume       = "abs/1301.2683",
 url          = "http://arxiv.org/abs/1301.2683",
 note         = "Accepted to PAAR'14.",
)
@article(abs-1109-0616,
 author       = "Josef Urban and Piotr Rudnicki and Geoff Sutcliffe",
 year         = "2013",
 title        = "{ATP} and Presentation Service for {Mizar} Formalizations",
 journal      = "J. Autom. Reasoning",
 volume       = "50",
 pages        = "229--241",
 doi          = "10.1007/s10817-012-9269-y",
)
@inproceedings(US+08,
 author       = "Josef Urban and Geoff Sutcliffe and Petr Pudl{\'a}k and Ji\v {r}\'{\i } Vysko\v {c}il",
 year         = "2008",
 title        = "{MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance}",
 editor       = "Alessandro Armando and Peter Baumgartner and Gilles Dowek",
 booktitle    = "IJCAR",
 series       = "LNCS",
 volume       = "5195",
 publisher    = "Springer",
 pages        = "441--456",
 url          = "http://dx.doi.org/10.1007/978-3-540-71070-7_37",
)
@inproceedings(UrbanV13,
 author       = "Josef Urban and Ji\v {r}\'{\i } Vysko\v {c}il",
 year         = "2013",
 title        = "Theorem Proving in Large Formal Mathematics as an Emerging {AI} Field",
 editor       = "Maria Paola Bonacina and Mark E. Stickel",
 booktitle    = "Automated Reasoning and Mathematics: Essays in Memory of William McCune",
 series       = "LNAI",
 volume       = "7788",
 publisher    = "Springer",
 pages        = "240--257",
 doi          = "10.1007/978-3-642-36675-8_13",
)
@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 C{\'e}sar A. Mu{\~n}oz and Sofi{\`e}ne Tahar",
 booktitle    = "TPHOLs",
 series       = "Lecture Notes in Computer Science",
 volume       = "5170",
 publisher    = "Springer",
 pages        = "33--38",
 url          = "http://dx.doi.org/10.1007/978-3-540-71067-7_7",
)