|
|
|
||
Last update: doc. Mgr. Petr Kaplický, Ph.D. (19.02.2019)
|
|
||
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (11.06.2019)
Předmět je zakončen ústní zkouškou. |
|
||
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (21.05.2021)
Cezary Kaliszyk, Josef Urban: Learning-Assisted Automated Reasoning with Flyspeck. J. Autom. Reasoning 53(2): 173-213 (2014)
John Harrison, Josef Urban, Freek Wiedijk: History of Interactive Theorem Proving. Computational Logic 2014: 135-214
John Harrison: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press 2009, ISBN 978-0-521-89957-4, pp. I-XIX, 1-681
Ian Goodfellow and Yoshua Bengio and Aaron Courville: Deep Learning. MIT Press 2016.
Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Miroslav Olsák: Reinforcement Learning of Theorem Proving. NeurIPS 2018: 8836-8847
Alexander A. Alemi, François Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, Josef Urban: DeepMath - Deep Sequence Models for Premise Selection. NIPS 2016: 2235-2243
Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, Michael Norrish: Learning to Prove with Tactics. CoRR abs/1804.00596 (2018)
Jan Jakubuv, Josef Urban: ENIGMA: Efficient Learning-Based Inference Guiding Machine. CICM 2017: 292-302 Mikolás Janota: Towards Generalization in QBF Solving via Machine Learning. AAAI 2018: 6607-6614
Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, Josef Urban: Hammering towards QED. J. Formalized Reasoning 9(1): 101-148 (2016)
Josef Urban, Jirí Vyskocil: Theorem Proving in Large Formal Mathematics as an Emerging AI Field. Automated Reasoning and Mathematics 2013: 240-257
Mikolas Janota, Martin Suda: Towards Smarter MACE-style Model Finders. LPAR 2018: 454-470 Cezary Kaliszyk, Josef Urban, Jirí Vyskocil: Efficient Semantic Features for Automated Reasoning over Large Theories. IJCAI 2015: 3084-3090
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil: Automating Formalization by Statistical and Semantic Parsing of Mathematics. ITP 2017: 12-27
Qingxiang Wang, Cezary Kaliszyk, Josef Urban: First Experiments with Neural Translation of Informal to Formal Mathematics. CoRR abs/1805.06502 (2018)
Karel Chvalovsky: Top-Down Neural Model For Formulae. ICLR 2019, https://openreview.net/pdf?id=Byg5QhR5FQ
Jan Jakubuv, Josef Urban: Hierarchical invention of theorem proving strategies. AI Commun. 31(3): 237-250 (2018)
Josef Urban, Geoff Sutcliffe, Petr Pudlák, Jirí Vyskocil: MaLARea SG1- Machine Learner for Automated Reasoning with Semantic Guidance. IJCAR 2008: 441-456
http://arg.ciirc.cvut.cz/teaching/mlr19/ |
|
||
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (27.02.2021)
Will be specified later. |
|
||
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (21.05.2021)
|