Josef Urban

Cited by

	All	Since 2018
Citations	5629	3509
h-index	41	33
i10-index	97	71

800

400

200

600

20062007200820092010201120122013201420152016201720182019202020212022202327 67 48 33 45 83 139 230 254 333 340 431 547 682 500 795 456 526

Public access

View all

63 articles

0 articles

available

not available

Based on funding mandates

Co-authors

Cezary KaliszykUniversity of InnsbruckVerified email at uibk.ac.at
Jan JakubuvCzech Technical University in Prague, CIIRCVerified email at cvut.cz
Jiří VyskočilCzech Technical University in PragueVerified email at cvut.cz
Daniel KuehlweinCapgeminiVerified email at cs.ru.nl
Geoff SutcliffeDepartment of Computer Science, University of MiamiVerified email at cs.miami.edu
Thibault GauthierCzech Technical University in PragueVerified email at thibaultgauthier.fr
Tom HeskesProfessor of Computer Science and Artificial Intelligence, Radboud University NijmegenVerified email at science.ru.nl
Bartosz PiotrowskiUniversity of Warsaw, Czech Technical UniversityVerified email at post.pl
Herman GeuversRadboud University Nijmegen, the NetherlandsVerified email at cs.ru.nl
Jasmin BlanchetteLudwig-Maximilians-Universität MünchenVerified email at ifi.lmu.de
Zarathustra GoertzelCIIRC/CVUT/Global MindVerified email at cvut.cz
Stephan SchulzProfessor of Computer Science, DHBW StuttgartVerified email at eprover.org
Michael KohlhaseInformatik, FAU Erlangen-NürnbergVerified email at fau.de
Zsolt ZomboriVerified email at renyi.hu
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
Martin SudaCzech Technical University in PragueVerified email at cvut.cz
Adam PeaseOwner, Articulate SoftwareVerified email at articulatesoftware.com
David StanovskyCharles UniversityVerified email at karlin.mff.cuni.cz
Krystof HoderGoogleVerified email at google.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, e2, 2017	386	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	241	2015
Hammering towards QED JC Blanchette, C Kaliszyk, LC Paulson, J Urban Journal of Formalized Reasoning 9 (1), 101-148, 2016	203	2016
Learning-assisted automated reasoning with Flyspeck C Kaliszyk, J Urban Journal of Automated Reasoning 53, 173-213, 2014	185	2014
MPTP 0.2: Design, implementation, and initial experiments J Urban Journal of Automated Reasoning 37, 21-43, 2006	166	2006
MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance J Urban, G Sutcliffe, P Pudlák, J Vyskočil Automated Reasoning: 4th International Joint Conference, IJCAR 2008 Sydney …, 2008	160	2008
Reinforcement learning of theorem proving C Kaliszyk, J Urban, H Michalewski, M Olšák Advances in Neural Information Processing Systems 31, 2018	159	2018
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, 191-213, 2014	157	2014
Mizar 40 for mizar 40 C Kaliszyk, J Urban Journal of Automated Reasoning 55 (3), 245-256, 2015	156	2015
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	131	2016
HOL(y)Hammer: Online ATP Service for HOL Light C Kaliszyk, J Urban Mathematics in Computer Science 9, 5-22, 2015	110	2015
Learning to Reason with HOL4 tactics T Gauthier, C Kaliszyk, J Urban arXiv preprint arXiv:1804.00595, 2018	105*	2018
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	103	2016
MaSh: machine learning for Sledgehammer D Kühlwein, JC Blanchette, C Kaliszyk, J Urban Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes …, 2013	102	2013
History of Interactive Theorem Proving. J Harrison, J Urban, F Wiedijk Computational Logic 9, 135-214, 2014	101	2014
ENIGMA: efficient learning-based inference guiding machine J Jakubův, J Urban Intelligent Computer Mathematics: 10th International Conference, CICM 2017 …, 2017	92	2017
XML-izing Mizar: making semantic processing and presentation of MML easy J Urban International Conference on Mathematical Knowledge Management, 346-360, 2005	89	2005
MoMM—fast interreduction and retrieval in large libraries of formalized mathematics J Urban International Journal on Artificial Intelligence Tools 15 (01), 109-130, 2006	87	2006
MaLeCoP Machine Learning Connection Prover J Urban, J Vyskočil, P Štěpánek Automated Reasoning with Analytic Tableaux and Related Methods: 20th …, 2011	86	2011
ATP and presentation service for Mizar formalizations J Urban, P Rudnicki, G Sutcliffe Journal of automated reasoning 50 (2), 229-241, 2013	85	2013

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

Cited by

Co-authors