Author:Josef Urban

Publications
Stateful Premise Selection by Recurrent Neural Networks Bartosz Piotrowski and Josef Urban In:LPAR23. LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Tactic Learning and Proving for the Coq Proof Assistant Lasse Blaauwbroek, Josef Urban and Herman Geuvers In:LPAR23. LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning
ProofWatch Meets ENIGMA: First Experiments Zarathustra Goertzel, Jan Jakubuv and Josef Urban In:LPAR-22 Workshop and Short Paper Proceedings
AI at CADE/IJCAR Josef Urban In:ARCADE 2017. 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements
Automated Invention of Strategies and Term Orderings for Vampire Jan Jakubuv, Martin Suda and Josef Urban In:GCAI 2017. 3rd Global Conference on Artificial Intelligence
TacticToe: Learning to Reason with HOL4 Tactics Thibault Gauthier, Cezary Kaliszyk and Josef Urban In:LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Improving Statistical Linguistic Algorithms for Parsing Mathematics Cezary Kaliszyk, Josef Urban and Jiri Vyskocil In:IWIL-2015. 11th International Workshop on the Implementation of Logics
Experiments with State-of-the-art Automated Provers on Problems in Tarskian Geometry Josef Urban and Robert Veroff In:IWIL-2015. 11th International Workshop on the Implementation of Logics
BliStr: The Blind Strategymaker Josef Urban In:GCAI 2015. Global Conference on Artificial Intelligence
Machine Learner for Automated Reasoning 0.4 and 0.5 Cezary Kaliszyk, Josef Urban and Jiri Vyskocil In:PAAR-2014. 4th Workshop on Practical Aspects of Automated Reasoning
Machine Learning of Coq Proof Guidance: First Experiments Cezary Kaliszyk, Lionel Mamane and Josef Urban In:SCSS 2014. 6th International Symposium on Symbolic Computation in Software Science
Learning from Multiple Proofs: First Experiments Daniel Kuehlwein and Josef Urban In:PAAR-2012. Third Workshop on Practical Aspects of Automated Reasoning
Initial Experiments with External Provers and Premise Selection on HOL Light Corpora Cezary Kaliszyk and Josef Urban In:PAAR-2012. Third Workshop on Practical Aspects of Automated Reasoning
PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving Jasmin Christian Blanchette and Josef Urban (editors) EPiC Series in Computing, volume 14
Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution Cezary Kaliszyk and Josef Urban In:PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving

Keyphrases

A* proof search, Artificial Intelligence², ATP Competitions, automated reasoning⁶, automated theorem proving⁵, automatic theorem provers, CADE, computational linguistics, Coq², feature weighting, first-order logic, Flyspeck², formal mathematics², higher-order logic², HOL Light³, IJCAR, interactive theorem proving³, large theories², large-theory automated reasoning², machine learning⁸, Mizar, multiple proofs, Parameters Learning, Parsing Mathematics, premise selection², proof advice, proof automation, Proof synthesis, proving strategy, Recurrent Neural Networks, strategy development, Strategy evolution, strategy invention, Tactic Search, Tarskian Geometry, type checking, type theory.