Author:Josef Urban

Publications
PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving Jasmin Christian Blanchette and Josef Urban (editors) EPiC Series in Computing, volume 14
Neural Conjecturing for Saturation Theorem Provers Karel Chvalovský, Martin Suda and Josef Urban In:Proceedings of 16th International Workshop on the Implementation on Logics. Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning (short papers)
Teaching Vampire New Tricks: An Experimental Study of Neural Clause Selection Karel Chvalovský, Martin Suda and Josef Urban In:Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning
First Experiments with Neural cvc5 Jelle Piepenbrock, Mikolas Janota, Josef Urban and Jan Jakubův In:Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning
Guiding an Instantiation Prover with Graph Neural Networks Karel Chvalovský, Konstantin Korovin, Jelle Piepenbrock and Josef Urban In:Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
A Mathematical Benchmark for Inductive Theorem Provers Thibault Gauthier, Chad Brown, Mikoláš Janota and Josef Urban In:Proceedings of 24th 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
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
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
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
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
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
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
Learning from Multiple Proofs: First Experiments Daniel Kuehlwein and Josef Urban In:PAAR-2012. Third Workshop on Practical Aspects of Automated Reasoning
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, arithmetic, Artificial Intelligence², ATP Competitions, automated reasoning⁷, automated theorem provers, automated theorem proving⁵, automatic theorem provers, benchmark, CADE, Clause Evaluation, computational linguistics, conjecturing, Coq², E prover, feature weighting, first-order logic, Flyspeck², formal mathematics², Graph Neural Networks, higher-order logic², HOL Light³, IJCAR, induction, inductive theorem provers, interactive theorem proving³, ITP hammers, large theories², large-theory automated reasoning², lemma introduction, machine learning¹¹, Mizar², multiple proofs, neural clause-selection guidance, OEIS, Parameters Learning, Parsing Mathematics, premise selection², proof advice, proof automation, Proof synthesis, proving strategies, proving strategy, Recurrent Neural Networks, saturation-based theorem proving, strategy development, Strategy evolution, strategy invention, Tactic Search, Tarskian Geometry, theorem proving², type checking, type theory, Vampire².