Artigos com autorizações de acesso público - Josef UrbanSaiba mais
66 artigos disponíveis publicamente
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
Autorizações: US National Science Foundation
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
Autorizações: European Commission
Hammering towards QED
JC Blanchette, C Kaliszyk, LC Paulson, J Urban
Journal of Formalized Reasoning 9 (1), 101-148, 2016
Autorizações: Austrian Science Fund, German Research Foundation, Netherlands Organisation …
Reinforcement learning of theorem proving
C Kaliszyk, J Urban, H Michalewski, M Olšák
Advances in Neural Information Processing Systems 31, 2018
Autorizações: European Commission
Learning to reason with hol4 tactics
T Gauthier, C Kaliszyk, J Urban
arXiv preprint arXiv:1804.00595, 2018
Autorizações: European Commission
HOL(y)Hammer: Online ATP Service for HOL Light
C Kaliszyk, J Urban
Mathematics in Computer Science 9, 5-22, 2015
Autorizações: Austrian Science Fund
MaSh: machine learning for Sledgehammer
D Kühlwein, JC Blanchette, C Kaliszyk, J Urban
Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes …, 2013
Autorizações: German Research Foundation
ENIGMA: efficient learning-based inference guiding machine
J Jakubův, J Urban
Intelligent Computer Mathematics: 10th International Conference, CICM 2017 …, 2017
Autorizações: European Commission
ENIGMA-NG: efficient neural and gradient-boosted inference guidance for E
K Chvalovský, J Jakubův, M Suda, J Urban
Automated Deduction–CADE 27: 27th International Conference on Automated …, 2019
Autorizações: European Commission
A learning-based fact selector for Isabelle/HOL
JC Blanchette, D Greenaway, C Kaliszyk, D Kühlwein, J Urban
Journal of Automated Reasoning 57, 219-244, 2016
Autorizações: Austrian Science Fund, German Research Foundation, Netherlands Organisation …
Efficient semantic features for automated reasoning over large theories
C Kaliszyk, J Urban, J Vyskocil
Palo Alto: AAAI Press, 2015
Autorizações: Austrian Science Fund
FEMaLeCoP: Fairly efficient machine learning connection prover
C Kaliszyk, J Urban
Logic for Programming, Artificial Intelligence, and Reasoning: 20th …, 2015
Autorizações: Austrian Science Fund, European Commission
ENIGMA anonymous: Symbol-independent inference guiding machine (system description)
J Jakubův, K Chvalovský, M Olšák, B Piotrowski, M Suda, J Urban
International Joint Conference on Automated Reasoning, 448-463, 2020
Autorizações: European Commission
TacticToe: learning to prove with tactics
T Gauthier, C Kaliszyk, J Urban, R Kumar, M Norrish
Journal of Automated Reasoning 65 (2), 257-286, 2021
Autorizações: European Commission
First experiments with neural translation of informal to formal mathematics
Q Wang, C Kaliszyk, J Urban
Intelligent Computer Mathematics: 11th International Conference, CICM 2018 …, 2018
Autorizações: European Commission
Exploration of neural machine translation in autoformalization of mathematics in Mizar
Q Wang, C Brown, C Kaliszyk, J Urban
Proceedings of the 9th ACM SIGPLAN International Conference on Certified …, 2020
Autorizações: European Commission
Learning-assisted theorem proving with millions of lemmas
C Kaliszyk, J Urban
Journal of symbolic computation 69, 109-128, 2015
Autorizações: Austrian Science Fund
Property invariant embedding for automated reasoning
M Olšák, C Kaliszyk, J Urban
ECAI 2020, 1395-1402, 2020
Autorizações: European Commission
The Mizar mathematical library in OMDoc: translation and applications
M Iancu, M Kohlhase, F Rabe, J Urban
Journal of Automated Reasoning 50 (2), 191-202, 2013
Autorizações: German Research Foundation
ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback
B Piotrowski, J Urban
Automated Reasoning: 9th International Joint Conference, IJCAR 2018, Held as …, 2018
Autorizações: European Commission
As informações de publicação e financiamento são determinadas automaticamente por um programa de computador