עקוב אחר
Josef Urban
Josef Urban
Distinguished Researcher at Czech Technical University in Prague
כתובת אימייל מאומתת בדומיין cvut.cz - דף הבית
כותרת
צוטט על ידי
צוטט על ידי
שנה
A formal proof of the Kepler conjecture‏
T Hales, M Adams, G Bauer, TD Dang, J Harrison, LT Hoang, C Kaliszyk, ...‏
Forum of mathematics, Pi 5, e2, 2017‏
5052017
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‏
288*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‏
2852015
Hammering towards QED‏
JC Blanchette, C Kaliszyk, LC Paulson, J Urban‏
Journal of Formalized Reasoning 9 (1), 101-148, 2016‏
2412016
Learning-assisted automated reasoning with Flyspeck‏
C Kaliszyk, J Urban‏
Journal of Automated Reasoning 53, 173-213, 2014‏
2052014
Reinforcement learning of theorem proving‏
C Kaliszyk, J Urban, H Michalewski, M Olšák‏
Advances in Neural Information Processing Systems 31, 2018‏
1992018
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‏
1842014
Mizar 40 for mizar 40‏
C Kaliszyk, J Urban‏
Journal of Automated Reasoning 55 (3), 245-256, 2015‏
1772015
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‏
1772008
MPTP 0.2: Design, implementation, and initial experiments‏
J Urban‏
Journal of Automated Reasoning 37, 21-43, 2006‏
1732006
History of interactive theorem proving‏
J Harrison, J Urban, F Wiedijk‏
Handbook of the History of Logic 9, 135-214, 2014‏
1452014
Learning to reason with hol4 tactics‏
T Gauthier, C Kaliszyk, J Urban‏
arXiv preprint arXiv:1804.00595, 2018‏
120*2018
HOL(y)Hammer: Online ATP Service for HOL Light‏
C Kaliszyk, J Urban‏
Mathematics in Computer Science 9, 5-22, 2015‏
1152015
MaSh: machine learning for Sledgehammer‏
D Kühlwein, JC Blanchette, C Kaliszyk, J Urban‏
Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes …, 2013‏
1152013
ENIGMA: efficient learning-based inference guiding machine‏
J Jakubův, J Urban‏
Intelligent Computer Mathematics: 10th International Conference, CICM 2017 …, 2017‏
1142017
MaLeCoP machine learning connection prover‏
J Urban, J Vyskočil, P Štěpánek‏
International Conference on Automated Reasoning with Analytic Tableaux and …, 2011‏
1002011
MPTP–motivation, implementation, first experiments‏
J Urban‏
Journal of Automated Reasoning 33, 319-339, 2004‏
902004
XML-izing Mizar: making semantic processing and presentation of MML easy‏
J Urban‏
International Conference on Mathematical Knowledge Management, 346-360, 2005‏
892005
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‏
882012
MoMM—fast interreduction and retrieval in large libraries of formalized mathematics‏
J Urban‏
International Journal on Artificial Intelligence Tools 15 (01), 109-130, 2006‏
882006
המערכת אינה יכולה לבצע את הפעולה כעת. נסה שוב מאוחר יותר.
מאמרים 1–20