Josef Urban

ORCID

Publication Activity (10 Years)

Years Active: 2000-2024
Publications (10 Years): 109

Top Venues

Publications

Jan Jakubuv, Mikolás Janota, Josef Urban
Solving Hard Mizar Problems with Instantiation and Strategy Invention. CoRR (2024)
Jelle Piepenbrock, Mikolas Janota, Josef Urban, Jan Jakubuv
First Experiments with Neural cvc5. LPAR (2024)
Jan Jakubuv, Mikolás Janota, Josef Urban
Solving Hard Mizar Problems with Instantiation and Strategy Invention. CICM (2024)
Lasse Blaauwbroek, David M. Cerna, Thibault Gauthier, Jan Jakubuv, Cezary Kaliszyk, Martin Suda, Josef Urban
Learning Guided Automated Reasoning: A Brief Survey. Logics and Type Systems in Theory and Practice (2024)
Lasse Blaauwbroek, David M. Cerna, Thibault Gauthier, Jan Jakubuv, Cezary Kaliszyk, Martin Suda, Josef Urban
Learning Guided Automated Reasoning: A Brief Survey. CoRR (2024)
Jan Jakubuv, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban
MizAR 60 for Mizar 50. CoRR (2023)
Jan Jakubuv, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban
MizAR 60 for Mizar 50. ITP (2023)
Mario Carneiro, Chad E. Brown, Josef Urban
Automated Theorem Proving for Metamath. ITP (2023)
Chad Brown, Adam Pease, Josef Urban
Translating SUMO-K to Higher-Order Set Theory. CoRR (2023)
Karel Chvalovský, Konstantin Korovin, Jelle Piepenbrock, Josef Urban
Guiding an Instantiation Prover with Graph Neural Networks. LPAR (2023)
Thibault Gauthier, Miroslav Olsák, Josef Urban
Alien coding. Int. J. Approx. Reason. 162 (2023)
Thibault Gauthier, Miroslav Olsák, Josef Urban
Alien Coding. CoRR (2023)
Thibault Gauthier, Chad E. Brown, Mikolas Janota, Josef Urban
A Mathematical Benchmark for Inductive Theorem Provers. LPAR (2023)
Thibault Gauthier, Josef Urban
Learning Program Synthesis for Integer Sequences from Scratch. AAAI (2023)
Liao Zhang, Lasse Blaauwbroek, Cezary Kaliszyk, Josef Urban
Learning Proof Transformations and Its Applications in Interactive Theorem Proving. FroCoS (2023)
Thibault Gauthier, Chad E. Brown, Mikolas Janota, Josef Urban
A Mathematical Benchmark for Inductive Theorem Provers. CoRR (2023)
Chad E. Brown, Adam Pease, Josef Urban
Translating SUMO-K to Higher-Order Set Theory. FroCoS (2023)
Zarathustra Amadeus Goertzel, Jan Jakubuv, Cezary Kaliszyk, Miroslav Olsák, Jelle Piepenbrock, Josef Urban
The Isabelle ENIGMA. ITP (2022)
Zarathustra Amadeus Goertzel, Jan Jakubuv, Cezary Kaliszyk, Miroslav Olsák, Jelle Piepenbrock, Josef Urban
The Isabelle ENIGMA. CoRR (2022)
Kimberley Parsons Trommler, Matthias Hafner, Wolfgang Kellerer, Peter Merz, Sigurd Schuster, Josef Urban, Uwe Baeder, Bertram Gunzelmann, Andreas Kornbichler
Six Questions about 6G. CoRR (2022)
Jelle Piepenbrock, Tom Heskes, Mikolás Janota, Josef Urban
Guiding an Automated Theorem Prover with Neural Rewriting. IJCAR (2022)
Jelle Piepenbrock, Josef Urban, Konstantin Korovin, Miroslav Olsák, Tom Heskes, Mikolas Janota
Machine Learning Meets The Herbrand Universe. CoRR (2022)
Chad E. Brown, Cezary Kaliszyk, Thibault Gauthier, Josef Urban
Proofgold: Blockchain for Formal Methods. FMBC@CAV (2022)
Kimberley Parsons Trommler, Matthias Hafner, Wolfgang Kellerer, Peter Merz, Sigurd Schuster, Josef Urban, Uwe Baeder, Bertram Gunzelmann, Andreas Kornbichler
PREVIEW VERSION: Six Insights into 6G: Orientation and Input for Developing Your Strategic 6G Research Plan. CoRR (2022)
Zsolt Zombori, Josef Urban, Miroslav Olsák
The Role of Entropy in Guiding a Connection Prover. CoRR (2021)
Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban
Learning Theorem Proving Components. TABLEAUX (2021)
Jaroslav Macke, Jirí Sedlár, Miroslav Olsák, Josef Urban, Josef Sivic
Learning to solve geometric construction problems from images. CoRR (2021)
Michael Färber, Cezary Kaliszyk, Josef Urban
Machine Learning Guidance for Connection Tableaux. J. Autom. Reason. 65 (2) (2021)
Zsolt Zombori, Josef Urban, Miroslav Olsák
The Role of Entropy in Guiding a Connection Prover. TABLEAUX (2021)
Jelle Piepenbrock, Tom Heskes, Mikolás Janota, Josef Urban
Learning Equational Theorem Proving. CoRR (2021)
Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Prokop Cerný, Cezary Kaliszyk, Josef Urban
Online Machine Learning Techniques for Coq: A Comparison. CoRR (2021)
Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Prokop Cerný, Cezary Kaliszyk, Josef Urban
Online Machine Learning Techniques for Coq: A Comparison. CICM (2021)
Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, Michael Norrish
TacticToe: Learning to Prove with Tactics. J. Autom. Reason. 65 (2) (2021)
Jaroslav Macke, Jirí Sedlár, Miroslav Olsák, Josef Urban, Josef Sivic
Learning to Solve Geometric Construction Problems from Images. CICM (2021)
Zarathustra Amadeus Goertzel, Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban
Fast and Slow Enigmas and Parental Guidance. CoRR (2021)
Zarathustra Amadeus Goertzel, Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban
Fast and Slow Enigmas and Parental Guidance. FroCoS (2021)
Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, Josef Urban
Towards Finding Longer Proofs. TABLEAUX (2021)
Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban
Learning Theorem Proving Components. CoRR (2021)
Josef Urban, Jan Jakubuv
First Neural Conjecturing Datasets and Experiments. CICM (2020)
Zsolt Zombori, Josef Urban, Chad E. Brown
Prolog Technology Reinforcement Learning Prover. CoRR (2020)
Jan Jakubuv, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, Josef Urban
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description). CoRR (2020)
Jan Jakubuv, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, Josef Urban
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description). IJCAR (2) (2020)
Lasse Blaauwbroek, Josef Urban, Herman Geuvers
The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq. CoRR (2020)
Bartosz Piotrowski, Josef Urban
Stateful Premise Selection by Recurrent Neural Networks. LPAR (2020)
Lasse Blaauwbroek, Josef Urban, Herman Geuvers
Tactic Learning and Proving for the Coq Proof Assistant. CoRR (2020)
Lasse Blaauwbroek, Josef Urban, Herman Geuvers
Tactic Learning and Proving for the Coq Proof Assistant. LPAR (2020)
George Labahn, James H. Davenport, Josef Urban
Foreword. Math. Comput. Sci. 14 (3) (2020)
Bartosz Piotrowski, Josef Urban
Stateful Premise Selection by Recurrent Neural Networks. CoRR (2020)
Lasse Blaauwbroek, Josef Urban, Herman Geuvers
The Tactician - A Seamless, Interactive Tactic Learner and Prover for Coq. CICM (2020)
Josef Urban, Jan Jakubuv
First Neural Conjecturing Datasets and Experiments. CoRR (2020)
Zsolt Zombori, Josef Urban, Chad E. Brown
Prolog Technology Reinforcement Learning Prover - (System Description). IJCAR (2) (2020)
Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, Josef Urban
Exploration of neural machine translation in autoformalization of mathematics in Mizar. CPP (2020)
Miroslav Olsák, Cezary Kaliszyk, Josef Urban
Property Invariant Embedding for Automated Reasoning. ECAI (2020)
Bartosz Piotrowski, Josef Urban
Guiding Inferences in Connection Tableau by Recurrent Neural Networks. CICM (2020)
Zarathustra Amadeus Goertzel, Jan Jakubuv, Josef Urban
ENIGMAWatch: ProofWatch Meets ENIGMA. TABLEAUX (2019)
Bartosz Piotrowski, Josef Urban
Guiding Theorem Proving by Recurrent Neural Networks. CoRR (2019)
Karel Chvalovský, Jan Jakubuv, Martin Suda, Josef Urban
ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E. CoRR (2019)
Bartosz Piotrowski, Josef Urban, Chad E. Brown, Cezary Kaliszyk
Can Neural Networks Learn Symbolic Rewriting? CoRR (2019)
Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, Josef Urban
Towards Finding Longer Proofs. CoRR (2019)
Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, Josef Urban
Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar. CoRR (2019)
Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban
GRUNGE: A Grand Unified ATP Challenge. CoRR (2019)
Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban
GRUNGE: A Grand Unified ATP Challenge. CADE (2019)
Miroslav Olsák, Cezary Kaliszyk, Josef Urban
Property Invariant Embedding for Automated Reasoning. CoRR (2019)
Karel Chvalovský, Jan Jakubuv, Martin Suda, Josef Urban
ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E. CADE (2019)
Jan Jakubuv, Josef Urban
Hammering Mizar by Learning Clause Guidance. CoRR (2019)
Zarathustra Amadeus Goertzel, Jan Jakubuv, Josef Urban
ENIGMAWatch: ProofWatch Meets ENIGMA. CoRR (2019)
Jan Jakubuv, Josef Urban
Hammering Mizar by Learning Clause Guidance (Short Paper). ITP (2019)
Grzegorz Bancerek, Adam Naumowicz, Josef Urban
System Description: XSL-Based Translator of Mizar to LaTeX. CICM (2018)
Bartosz Piotrowski, Josef Urban
ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback. CoRR (2018)
Bartosz Piotrowski, Josef Urban
ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback. IJCAR (2018)
Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Miroslav Olsák
Reinforcement Learning of Theorem Proving. NeurIPS (2018)
Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, Michael Norrish
Learning to Prove with Tactics. CoRR (2018)
Qingxiang Wang, Cezary Kaliszyk, Josef Urban
First Experiments with Neural Translation of Informal to Formal Mathematics. CoRR (2018)
Thibault Gauthier, Cezary Kaliszyk, Josef Urban
Learning to Reason with HOL4 tactics. CoRR (2018)
Qingxiang Wang, Cezary Kaliszyk, Josef Urban
First Experiments with Neural Translation of Informal to Formal Mathematics. CICM (2018)
Zarathustra Amadeus Goertzel, Jan Jakubuv, Stephan Schulz, Josef Urban
ProofWatch: Watchlist Guidance for Large Theories in E. CoRR (2018)
Pascal Fontaine, Cezary Kaliszyk, Stephan Schulz, Josef Urban
Foreword to the Special Issue on Automated Reasoning. AI Commun. 31 (3) (2018)
Michael Färber, Cezary Kaliszyk, Josef Urban
Machine Learning Guidance and Proof Certification for Connection Tableaux. CoRR (2018)
Zarathustra Amadeus Goertzel, Jan Jakubuv, Stephan Schulz, Josef Urban
ProofWatch: Watchlist Guidance for Large Theories in E. ITP (2018)
Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Mirek Olsák
Reinforcement Learning of Theorem Proving. CoRR (2018)
Zarathustra Amadeus Goertzel, Jan Jakubuv, Josef Urban
ProofWatch Meets ENIGMA: First Experiments. LPAR (Workshop and Short Papers) (2018)
Jan Jakubuv, Josef Urban
Hierarchical invention of theorem proving strategies. AI Commun. 31 (3) (2018)
Jan Jakubuv, Josef Urban
Enhancing ENIGMA Given Clause Guidance. CICM (2018)
Michael Färber, Cezary Kaliszyk, Josef Urban
Monte Carlo Tableau Proof Search. CADE (2017)
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
Automating Formalization by Statistical and Semantic Parsing of Mathematics. ITP (2017)
Jan Jakubuv, Josef Urban
ENIGMA: Efficient Learning-Based Inference Guiding Machine. CICM (2017)
Stephan Schulz, Geoff Sutcliffe, Josef Urban, Adam Pease
Detecting Inconsistencies in Large First-Order Knowledge Bases. CADE (2017)
Jan Jakubuv, Josef Urban
BliStrTune: hierarchical invention of theorem proving strategies. CPP (2017)
Josef Urban
AI at CADE/IJCAR. ARCADE@CADE (2017)
Thibault Gauthier, Cezary Kaliszyk, Josef Urban
TacticToe: Learning to Reason with HOL4 Tactics. LPAR (2017)
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
System Description: Statistical Parsing of Informalized Mizar Formulas. SYNASC (2017)
Jan Jakubuv, Martin Suda, Josef Urban
Automated Invention of Strategies and Term Orderings for Vampire. GCAI (2017)
Jan Jakubuv, Josef Urban
ENIGMA: Efficient Learning-based Inference Guiding Machine. CoRR (2017)
Geoff Sutcliffe, Josef Urban
The CADE-25 Automated Theorem Proving system competition - CASC-25. AI Commun. 29 (3) (2016)
Thibault Gauthier, Cezary Kaliszyk, Josef Urban
Initial Experiments with Statistical Conjecturing over Large Formal Corpora. FM4M/MathUI/ThEdu/DP/WIP@CIKM (2016)
Josef Urban
Learning Intelligent Theorem Proving from Large Formal Corpora. ISAIM (2016)
Chad E. Brown, Josef Urban
Extracting Higher-Order Goals from the Mizar Mathematical Library. CoRR (2016)
Chad E. Brown, Josef Urban
Extracting Higher-Order Goals from the Mizar Mathematical Library. CICM (2016)
Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, Josef Urban
A Learning-Based Fact Selector for Isabelle/HOL. J. Autom. Reason. 57 (3) (2016)
Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
Semantic Parsing of Mathematics by Context-based Learning from Aligned Corpora and Theorem Proving. CoRR (2016)

Josef Urban.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Josef Urban