Josef Urban

Cited by

	All	Since 2019
Citations	6423	3728
h-index	43	31
i10-index	104	73

800

400

200

600

200620072008200920102011201220132014201520162017201820192020202120222023202427 67 49 31 45 80 142 227 253 337 342 432 552 601 538 796 463 787 532

Public access

View all

65 articles

0 articles

available

not available

Based on funding mandates

Co-authors

Cezary KaliszykUniversity of MelbourneVerified email at unimelb.edu.au
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
Thibault GauthierCzech Technical University in PragueVerified email at thibaultgauthier.fr
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
Bartosz PiotrowskiIDEAS NCBRVerified 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
Zsolt ZomboriResearcher, Alfréd Rényi Institute of MathematicsVerified email at renyi.hu
Michael KohlhaseInformatik, FAU Erlangen-NürnbergVerified email at fau.de
Karol PąkInstitute of Informatics, University of BialystokVerified email at uwb.edu.pl
Martin SudaCzech Technical University in PragueVerified email at cvut.cz
Artur KorniłowiczUniwersytet w BiałymstokuVerified email at math.uwb.edu.pl
Adam PeaseNaval Postgraduate SchoolVerified 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 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	474	2017
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	280*	2016
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	267	2015
Hammering towards QED JC Blanchette, C Kaliszyk, LC Paulson, J Urban Journal of Formalized Reasoning 9 (1), 101-148, 2016	228	2016
Learning-assisted automated reasoning with Flyspeck C Kaliszyk, J Urban Journal of Automated Reasoning 53, 173-213, 2014	205	2014
Reinforcement learning of theorem proving C Kaliszyk, J Urban, H Michalewski, M Olšák Advances in Neural Information Processing Systems 31, 2018	186	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	177	2014
Mizar 40 for mizar 40 C Kaliszyk, J Urban Journal of Automated Reasoning 55 (3), 245-256, 2015	174	2015
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	171	2008
MPTP 0.2: Design, implementation, and initial experiments J Urban Journal of Automated Reasoning 37, 21-43, 2006	170	2006
History of interactive theorem proving J Harrison, J Urban, F Wiedijk Handbook of the History of Logic 9, 135-214, 2014	126	2014
Learning to reason with hol4 tactics T Gauthier, C Kaliszyk, J Urban arXiv preprint arXiv:1804.00595, 2018	115*	2018
HOL(y)Hammer: Online ATP Service for HOL Light C Kaliszyk, J Urban Mathematics in Computer Science 9, 5-22, 2015	113	2015
ENIGMA: efficient learning-based inference guiding machine J Jakubův, J Urban Intelligent Computer Mathematics: 10th International Conference, CICM 2017 …, 2017	111	2017
MaSh: machine learning for Sledgehammer D Kühlwein, JC Blanchette, C Kaliszyk, J Urban Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes …, 2013	109	2013
MaLeCoP machine learning connection prover J Urban, J Vyskočil, P Štěpánek International Conference on Automated Reasoning with Analytic Tableaux and …, 2011	95	2011
MPTP–motivation, implementation, first experiments J Urban Journal of Automated Reasoning 33, 319-339, 2004	89	2004
Overview and evaluation of premise selection techniques for large theory mathematics D Kühlwein, T van Laarhoven, E Tsivtsivadze, J Urban, T Heskes Automated Reasoning: 6th International Joint Conference, IJCAR 2012 …, 2012	88	2012
XML-izing Mizar: making semantic processing and presentation of MML easy J Urban International Conference on Mathematical Knowledge Management, 346-360, 2005	88	2005
ATP and presentation service for Mizar formalizations J Urban, P Rudnicki, G Sutcliffe Journal of Automated Reasoning 50 (2), 229-241, 2013	86	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