Follow
Josef Urban
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
3532017
Mizar: State-of-the-art and beyond
G Bancerek, C Byliński, A Grabowski, A Korniłowicz, R Matuszewski, ...
Intelligent Computer Mathematics: International Conference, CICM 2015…, 2015
2212015
Hammering towards QED
JC Blanchette, C Kaliszyk, LC Paulson, J Urban
Journal of Formalized Reasoning 9 (1), 101-148, 2016
1872016
Learning-assisted automated reasoning with Flyspeck
C Kaliszyk, J Urban
Journal of Automated Reasoning 53, 173-213, 2014
1812014
MPTP 0.2: Design, implementation, and initial experiments
J Urban
Journal of Automated Reasoning 37, 21-43, 2006
1592006
MaLARea SG1--Machine learner for automated reasoning with semantic guidance
J Urban, G Sutcliffe, P Pudlk, J Vyskocil
Lecture Notes in Computer Science 5195, 441-456, 2008
1572008
Premise selection for mathematics by corpus analysis and kernel methods
J Alama, T Heskes, D Khlwein, E Tsivtsivadze, J Urban
Journal of automated reasoning 52, 191-213, 2014
1442014
Mizar 40 for mizar 40
C Kaliszyk, J Urban
Journal of Automated Reasoning 55 (3), 245-256, 2015
1432015
Reinforcement learning of theorem proving
C Kaliszyk, J Urban, H Michalewski, M Olšk
Advances in Neural Information Processing Systems 31, 2018
1422018
Deepmath-deep sequence models for premise selection
G Irving, C Szegedy, AA Alemi, N En, F Chollet, J Urban
Advances in neural information processing systems 29, 2016
1212016
HOL(y)Hammer: Online ATP Service for HOL Light
C Kaliszyk, J Urban
Mathematics in Computer Science 9, 5-22, 2015
1052015
Learning to Reason with HOL4 tactics
T Gauthier, C Kaliszyk, J Urban
arXiv preprint arXiv:1804.00595, 2018
98*2018
MaSh: machine learning for Sledgehammer
D Khlwein, JC Blanchette, C Kaliszyk, J Urban
Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes…, 2013
982013
DeepMath-deep sequence models for premise selection
AA Alemi, F Chollet, N En, G Irving, C Szegedy, J Urban
arXiv preprint arXiv:1606.04442, 2016
952016
XML-izing Mizar: making semantic processing and presentation of MML easy
J Urban
Mathematical Knowledge Management: 4th International Conference, MKM 2005…, 2006
882006
MoMM—fast interreduction and retrieval in large libraries of formalized mathematics
J Urban
International Journal on Artificial Intelligence Tools 15 (01), 109-130, 2006
872006
History of Interactive Theorem Proving.
J Harrison, J Urban, F Wiedijk
Computational Logic 9, 135-214, 2014
862014
ATP and presentation service for Mizar formalizations
J Urban, P Rudnicki, G Sutcliffe
Journal of automated reasoning 50 (2), 229-241, 2013
822013
MaLeCoP Machine Learning Connection Prover
J Urban, J Vyskočil, P Štěpnek
Automated Reasoning with Analytic Tableaux and Related Methods: 20th…, 2011
822011
MPTP–motivation, implementation, first experiments
J Urban
Journal of Automated Reasoning 33, 319-339, 2004
812004
The system can't perform the operation now. Try again later.
Articles 1–20