フォロー
Josef Urban
タイトル
引用先
引用先
年
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
4962017
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
293*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
2862015
Hammering towards QED
JC Blanchette, C Kaliszyk, LC Paulson, J Urban
Journal of Formalized Reasoning 9 (1), 101-148, 2016
2392016
Learning-assisted automated reasoning with Flyspeck
C Kaliszyk, J Urban
Journal of Automated Reasoning 53, 173-213, 2014
2072014
Reinforcement learning of theorem proving
C Kaliszyk, J Urban, H Michalewski, M Olšák
Advances in Neural Information Processing Systems 31, 2018
1952018
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
1822014
Mizar 40 for mizar 40
C Kaliszyk, J Urban
Journal of Automated Reasoning 55 (3), 245-256, 2015
1752015
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
1732008
MPTP 0.2: Design, implementation, and initial experiments
J Urban
Journal of Automated Reasoning 37, 21-43, 2006
1702006
History of interactive theorem proving
J Harrison, J Urban, F Wiedijk
Handbook of the History of Logic 9, 135-214, 2014
1432014
Learning to reason with hol4 tactics
T Gauthier, C Kaliszyk, J Urban
arXiv preprint arXiv:1804.00595, 2018
118*2018
HOL(y)Hammer: Online ATP Service for HOL Light
C Kaliszyk, J Urban
Mathematics in Computer Science 9, 5-22, 2015
1152015
ENIGMA: efficient learning-based inference guiding machine
J Jakubův, J Urban
Intelligent Computer Mathematics: 10th International Conference, CICM 2017 …, 2017
1142017
MaSh: machine learning for Sledgehammer
D Kühlwein, JC Blanchette, C Kaliszyk, J Urban
Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes …, 2013
1142013
MaLeCoP machine learning connection prover
J Urban, J Vyskočil, P Štěpánek
International Conference on Automated Reasoning with Analytic Tableaux and …, 2011
982011
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
892012
MPTP–motivation, implementation, first experiments
J Urban
Journal of Automated Reasoning 33, 319-339, 2004
892004
XML-izing Mizar: making semantic processing and presentation of MML easy
J Urban
International Conference on Mathematical Knowledge Management, 346-360, 2005
882005
ATP and presentation service for Mizar formalizations
J Urban, P Rudnicki, G Sutcliffe
Journal of Automated Reasoning 50 (2), 229-241, 2013
862013
現在システムで処理を実行できません。しばらくしてからもう一度お試しください。
論文 1–20