Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze & Josef Urban (2014):
Premise Selection for Mathematics by Corpus Analysis and Kernel Methods.
J. Autom. Reasoning 52(2),
pp. 191–213,
doi:10.1007/s10817-013-9286-5.
Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu & Nicholas Smallbone (2013):
Encoding Monomorphic and Polymorphic Types.
In: Nir Piterman & Scott A. Smolka: TACAS,
Lecture Notes in Computer Science 7795.
Springer,
pp. 493–507.
Available at http://dx.doi.org/10.1007/978-3-642-36742-7_34.
Adam Grabowski, Artur Korniłowicz & Adam Naumowicz (2010):
Mizar in a Nutshell.
Journal of Formalized Reasoning 3(2),
pp. 153–245.
Thomas C. Hales (2006):
Introduction to the Flyspeck Project.
In: Thierry Coquand, Henri Lombardi & Marie-Françoise Roy: Mathematics, Algorithms, Proofs,
Dagstuhl Seminar Proceedings 05021.
Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany,
Dagstuhl, Germany,
pp. 1–11.
Available at http://drops.dagstuhl.de/opus/volltexte/2006/432.
John Harrison (1996):
HOL Light: A Tutorial Introduction.
In: Mandayam K. Srivas & Albert John Camilleri: FMCAD,
LNCS 1166.
Springer,
pp. 265–269.
Available at http://dx.doi.org/10.1007/BFb0031814.
Krystof Hoder & Andrei Voronkov (2011):
Sine Qua Non for Large Theory Reasoning.
In: Nikolaj Bjørner & Viorica Sofronie-Stokkermans: CADE,
LNCS 6803.
Springer,
pp. 299–314.
Available at http://dx.doi.org/10.1007/978-3-642-22438-6_23.
Cezary Kaliszyk & Josef Urban (2013):
HOL(y)Hammer: Online ATP Service for HOL Light.
CoRR abs/1309.4962.
Available at http://arxiv.org/abs/1309.4962.
Accepted for publication in Mathematics in Computer Science.
Cezary Kaliszyk & Josef Urban (2013):
MizAR 40 for Mizar 40.
CoRR abs/1310.2805.
Available at http://arxiv.org/abs/1310.2805.
Cezary Kaliszyk & Josef Urban (2013):
Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution.
In: Jasmin Christian Blanchette & Josef Urban: PxTP 2013,
EPiC Series 14.
EasyChair,
pp. 87–95.
Cezary Kaliszyk & Josef Urban (2014):
Learning-assisted Automated Reasoning with Flyspeck.
Journal of Automated Reasoning,
doi:10.1007/s10817-014-9303-3.
http://dx.doi.org/10.1007/s10817-014-9303-3.
Cezary Kaliszyk, Josef Urban & Jiří Vyskočil (2014):
Machine Learner for Automated Reasoning 0.4 and 0.5.
CoRR abs/1402.2359.
Available at http://arxiv.org/abs/1402.2359.
Accepted to PAAR'14.
Matt Kaufmann & J Strother Moore (1998):
A precise description of the ACL2 logic.
http://www.cs.utexas.edu/users/moore/publications/km97a.pdf.
Laura Kovács & Andrei Voronkov (2013):
First-Order Theorem Proving and Vampire.
In: Natasha Sharygina & Helmut Veith: CAV,
Lecture Notes in Computer Science 8044.
Springer,
pp. 1–35.
Available at http://dx.doi.org/10.1007/978-3-642-39799-8_1.
Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk & Josef Urban (2013):
MaSh: Machine Learning for Sledgehammer.
In: Sandrine Blazy, Christine Paulin-Mohring & David Pichardie: Proc. of the 4th International Conference on Interactive Theorem Proving (ITP'13),
LNCS 7998.
Springer,
pp. 35–50,
doi:10.1007/978-3-642-39634-2_6.
Available at http://cl-informatik.uibk.ac.at/users/cek/docs/kuehlwein-itp13.pdf.
Daniel Kühlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban & Tom Heskes (2012):
Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics.
In: Bernhard Gramlich, Dale Miller & Uli Sattler: IJCAR,
LNCS 7364.
Springer,
pp. 378–392.
Available at http://dx.doi.org/10.1007/978-3-642-31365-3_30.
Jia Meng & Lawrence C. Paulson (2008):
Translating Higher-Order Clauses to First-Order Clauses.
J. Autom. Reasoning 40(1),
pp. 35–60.
Available at http://dx.doi.org/10.1007/s10817-007-9085-y.
Jia Meng & Lawrence C. Paulson (2009):
Lightweight relevance filtering for machine-generated resolution problems.
J. Applied Logic 7(1),
pp. 41–57.
Available at http://dx.doi.org/10.1016/j.jal.2007.07.004.
Leonardo Mendonça de Moura & Nikolaj Bjørner (2008):
Z3: An Efficient SMT Solver.
In: C. R. Ramakrishnan & Jakob Rehof: TACAS,
LNCS 4963.
Springer,
pp. 337–340.
Available at http://dx.doi.org/10.1007/978-3-540-78800-3_24.
D. Ramachandran, Reagan P. & K. Goolsbey (2005):
First-orderized ResearchCyc: Expressiveness and Efficiency in a Common Sense Knowledge Base.
In: Shvaiko P.: Proceedings of the Workshop on Contexts and Ontologies: Theory, Practice and Applications.
Geoff Sutcliffe (2013):
The 6th IJCAR automated theorem proving system competition - CASC-J6.
AI Commun. 26(2),
pp. 211–223.
Available at http://dx.doi.org/10.3233/AIC-130550.
Josef Urban (2004):
MPTP - Motivation, Implementation, First Experiments.
Journal of Automated Reasoning 33(3-4),
pp. 319–339,
doi:10.1007/s10817-004-6245-1.
Josef Urban (2014):
BliStr: The Blind Strategymaker.
CoRR abs/1301.2683.
Available at http://arxiv.org/abs/1301.2683.
Accepted to PAAR'14..
Josef Urban, Piotr Rudnicki & Geoff Sutcliffe (2013):
ATP and Presentation Service for Mizar Formalizations.
J. Autom. Reasoning 50,
pp. 229–241,
doi:10.1007/s10817-012-9269-y.
Josef Urban, Geoff Sutcliffe, Petr Pudlák & JiříVyskočil (2008):
MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance.
In: Alessandro Armando, Peter Baumgartner & Gilles Dowek: IJCAR,
LNCS 5195.
Springer,
pp. 441–456.
Available at http://dx.doi.org/10.1007/978-3-540-71070-7_37.
Josef Urban & JiříVyskočil (2013):
Theorem Proving in Large Formal Mathematics as an Emerging AI Field.
In: Maria Paola Bonacina & Mark E. Stickel: Automated Reasoning and Mathematics: Essays in Memory of William McCune,
LNAI 7788.
Springer,
pp. 240–257,
doi:10.1007/978-3-642-36675-8_13.
Makarius Wenzel, Lawrence C. Paulson & Tobias Nipkow (2008):
The Isabelle Framework.
In: Otmane Aït Mohamed, César A. Muñoz & Sofiène Tahar: TPHOLs,
Lecture Notes in Computer Science 5170.
Springer,
pp. 33–38.
Available at http://dx.doi.org/10.1007/978-3-540-71067-7_7.
eptcs@eptcs.org