Josef Urban

Cited by

	All	Since 2017
Citations	4816	3129
h-index	37	30
i10-index	94	71

800

400

200

600

2006200720082009201020112012201320142015201620172018201920202021202226 67 48 32 45 84 130 211 290 326 336 428 557 672 502 784 180

Public access

View all

71 articles

1 article

available

not available

Based on funding mandates

Co-authors

Cezary KaliszykUniversity of InnsbruckVerified email at uibk.ac.at
Jiří VyskočilCzech Technical University in PragueVerified email at cvut.cz
Jan JakubuvCzech Technical University in Prague, CIIRCVerified email at cvut.cz
Daniel KuehlweinCapgeminiVerified email at cs.ru.nl
Geoff SutcliffeDepartment of Computer Science, University of MiamiVerified email at cs.miami.edu
Tom HeskesProfessor of Computer Science and Artificial Intelligence, Radboud University NijmegenVerified email at science.ru.nl
Herman GeuversRadboud University Nijmegen, the NetherlandsVerified email at cs.ru.nl
Jasmin BlanchetteVrije Universiteit AmsterdamVerified email at vu.nl
Stephan SchulzProfessor of Computer Science, DHBW StuttgartVerified email at eprover.org
Michael KohlhaseInformatik, FAU Erlangen-NürnbergVerified email at fau.de
Karol PąkInstitute of Informatics, University of BialystokVerified email at uwb.edu.pl
Artur KorniłowiczUniwersytet w BiałymstokuVerified email at math.uwb.edu.pl
David StanovskyCharles UniversityVerified email at karlin.mff.cuni.cz
Krystof HoderGoogleVerified email at google.com
Yury PuzisCOO at Charmtech LabsVerified email at cs.sunysb.edu
Sebastiaan J. C. JoostenLecturer, Dartmouth CollegeVerified email at dartmouth.edu
Christoph LangeFraunhofer FIT, GermanyVerified email at fit.fraunhofer.de
Carst TankinkSoftware engineer - Bol.com

Josef Urban

Distinguished Researcher at Czech Technical University in Prague

Verified email at cvut.cz - Homepage

Automated Reasoning Artificial Intelligence Semantic Knowledge Bases Formal Mathematics Machine Learning


Title Sort by citations Sort by year Sort by title	Cited by Cited by	Year
A formal proof of the Kepler conjecture T Hales, M Adams, G Bauer, TD Dang, J Harrison, H Le Truong, ... Forum of mathematics, Pi 5, 2017	329	2017
Mizar: State-of-the-art and beyond G Bancerek, C Byliński, A Grabowski, A Korniłowicz, R Matuszewski, ... International Conference on Intelligent Computer Mathematics, 261-279, 2015	184	2015
Learning-assisted automated reasoning with Flyspeck C Kaliszyk, J Urban Journal of Automated Reasoning 53 (2), 173-213, 2014	174	2014
Hammering towards QED JC Blanchette, C Kaliszyk, LC Paulson, J Urban Journal of Formalized Reasoning 9 (1), 101-148, 2016	168	2016
MPTP 0.2: Design, implementation, and initial experiments J Urban Journal of Automated Reasoning 37 (1), 21-43, 2006	155	2006
MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance J Urban, G Sutcliffe, P Pudlák, J Vyskočil International Joint Conference on Automated Reasoning, 441-456, 2008	150	2008
Mizar 40 for mizar 40 C Kaliszyk, J Urban Journal of Automated Reasoning 55 (3), 245-256, 2015	136	2015
Premise selection for mathematics by corpus analysis and kernel methods J Alama, T Heskes, D Kühlwein, E Tsivtsivadze, J Urban Journal of automated reasoning 52 (2), 191-213, 2014	134	2014
Reinforcement learning of theorem proving C Kaliszyk, J Urban, H Michalewski, M Olšák Advances in Neural Information Processing Systems 31, 2018	116	2018
Deepmath-deep sequence models for premise selection G Irving, C Szegedy, AA Alemi, N Eén, F Chollet, J Urban Advances in neural information processing systems 29, 2016	108	2016
HOL (y) Hammer: Online ATP service for HOL Light C Kaliszyk, J Urban Mathematics in Computer Science 9 (1), 5-22, 2015	98	2015
MaSh: machine learning for Sledgehammer D Kühlwein, JC Blanchette, C Kaliszyk, J Urban International Conference on Interactive Theorem Proving, 35-50, 2013	95	2013
Learning to Reason with HOL4 tactics T Gauthier, C Kaliszyk, J Urban arXiv preprint arXiv:1804.00595, 2018	93*	2018
MoMM—fast interreduction and retrieval in large libraries of formalized mathematics J Urban International Journal on Artificial Intelligence Tools 15 (01), 109-130, 2006	88	2006
XML-izing Mizar: making semantic processing and presentation of MML easy J Urban International Conference on Mathematical Knowledge Management, 346-360, 2005	88	2005
DeepMath-deep sequence models for premise selection AA Alemi, F Chollet, N Eén, G Irving, C Szegedy, J Urban arXiv preprint arXiv:1606.04442, 2016	87	2016
MaLeCoP machine learning connection prover J Urban, J Vyskočil, P Štěpánek International Conference on Automated Reasoning with Analytic Tableaux and …, 2011	82	2011
MPTP–motivation, implementation, first experiments J Urban Journal of Automated Reasoning 33 (3), 319-339, 2004	80	2004
ATP and presentation service for Mizar formalizations J Urban, P Rudnicki, G Sutcliffe Journal of automated reasoning 50 (2), 229-241, 2013	77	2013
Overview and evaluation of premise selection techniques for large theory mathematics D Kühlwein, T Laarhoven, E Tsivtsivadze, J Urban, T Heskes International Joint Conference on Automated Reasoning, 378-392, 2012	75	2012

The system can't perform the operation now. Try again later.

Articles 1–20

Citations per year

Duplicate citations

Merged citations

Add co-authorsCo-authors

Follow this author

Cited by

Co-authors