Josef Urban
Titel
Geciteerd door
Geciteerd door
Jaar
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, 2017
1832017
Mizar: State-of-the-art and beyond
G Bancerek, C Byliński, A Grabowski, A Korniłowicz, R Matuszewski, ...
Conferences on Intelligent Computer Mathematics, 261-279, 2015
1402015
Learning-assisted automated reasoning with Flyspeck
C Kaliszyk, J Urban
Journal of Automated Reasoning 53 (2), 173-213, 2014
1382014
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
1212008
MPTP 0.2: Design, implementation, and initial experiments
J Urban
Journal of Automated Reasoning 37 (1-2), 21-43, 2006
1172006
Hammering towards QED
JC Blanchette, C Kaliszyk, LC Paulson, J Urban
Journal of Formalized Reasoning 9 (1), 101-148, 2016
1062016
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, 2235-2243, 2016
1032016
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 (2), 191-213, 2014
972014
Mizar 40 for mizar 40
C Kaliszyk, J Urban
Journal of Automated Reasoning 55 (3), 245-256, 2015
932015
MaSh: machine learning for sledgehammer
D Kühlwein, JC Blanchette, C Kaliszyk, J Urban
International Conference on Interactive Theorem Proving, 35-50, 2013
822013
MoMM—Fast interreduction and retrieval in large libraries of formalized mathematics
J Urban
International Journal on Artificial Intelligence Tools 15 (01), 109-130, 2006
782006
XML-izing Mizar: making semantic processing and presentation of MML easy
J Urban
International Conference on Mathematical Knowledge Management, 346-360, 2005
772005
HOL (y) Hammer: Online ATP service for HOL Light
C Kaliszyk, J Urban
Mathematics in Computer Science 9 (1), 5-22, 2015
712015
MPTP–motivation, implementation, first experiments
J Urban
Journal of Automated Reasoning 33 (3-4), 319-339, 2004
642004
ATP and presentation service for Mizar formalizations
J Urban, P Rudnicki, G Sutcliffe
Journal of Automated Reasoning 50 (2), 229-241, 2013
612013
MaLeCoP machine learning connection prover
J Urban, J Vyskočil, P Štěpánek
International Conference on Automated Reasoning with Analytic Tableaux and …, 2011
602011
Overview and evaluation of premise selection techniques for large theory mathematics
D Kühlwein, T van Laarhoven, E Tsivtsivadze, J Urban, T Heskes
International Joint Conference on Automated Reasoning, 378-392, 2012
592012
MizarMode—an integrated proof assistance tool for the Mizar way of formalizing mathematics
J Urban
Journal of Applied Logic 4 (4), 414-427, 2006
552006
MaLARea: a Metasystem for Automated Reasoning in Large Theories.
J Urban
ESARLT 257, 2007
512007
FEMaLeCoP: Fairly efficient machine learning connection prover
C Kaliszyk, J Urban
Logic for Programming, Artificial Intelligence, and Reasoning, 88-96, 2015
492015
Het systeem kan de bewerking nu niet uitvoeren. Probeer het later opnieuw.
Artikelen 1–20