Josef Urban

Cited by

	All	Since 2020
Citations	6643	3358
h-index	43	30
i10-index	105	66

800

400

200

600

2006200720082009201020112012201320142015201620172018201920202021202220232024202527 67 49 31 45 80 142 227 249 333 346 433 554 601 544 791 459 793 707 62

Public access

View all

66 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
Martin SudaCzech Technical University in PragueVerified email at cvut.cz
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
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	494	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	292*	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	286	2015
Hammering towards QED JC Blanchette, C Kaliszyk, LC Paulson, J Urban Journal of Formalized Reasoning 9 (1), 101-148, 2016	238	2016
Learning-assisted automated reasoning with Flyspeck C Kaliszyk, J Urban Journal of Automated Reasoning 53, 173-213, 2014	207	2014
Reinforcement learning of theorem proving C Kaliszyk, J Urban, H Michalewski, M Olšák Advances in Neural Information Processing Systems 31, 2018	194	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	182	2014
Mizar 40 for mizar 40 C Kaliszyk, J Urban Journal of Automated Reasoning 55 (3), 245-256, 2015	175	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	173	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	142	2014
Learning to reason with hol4 tactics T Gauthier, C Kaliszyk, J Urban arXiv preprint arXiv:1804.00595, 2018	118*	2018
ENIGMA: efficient learning-based inference guiding machine J Jakubův, J Urban Intelligent Computer Mathematics: 10th International Conference, CICM 2017 …, 2017	114	2017
HOL(y)Hammer: Online ATP Service for HOL Light C Kaliszyk, J Urban Mathematics in Computer Science 9, 5-22, 2015	114	2015
MaSh: machine learning for Sledgehammer D Kühlwein, JC Blanchette, C Kaliszyk, J Urban Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes …, 2013	114	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	97	2011
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	89	2012
MPTP–motivation, implementation, first experiments J Urban Journal of Automated Reasoning 33, 319-339, 2004	89	2004
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