default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDJosef Urban
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2025
[j26]Jelle Piepenbrock
, Josef Urban, Konstantin Korovin, Miroslav Olsák, Tom Heskes, Mikolás Janota:
Invariant neural architecture for learning term synthesis in instantiation proving. J. Symb. Comput. 128: 102375 (2025)- 2024
- [c109]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: 54-83 - [c108]Jan Jakubuv, Mikolás Janota, Jelle Piepenbrock, Josef Urban:
Machine Learning for Quantifier Selection in cvc5. ECAI 2024: 4336-4343 - [c107]Jelle Piepenbrock, Mikolas Janota, Josef Urban, Jan Jakubuv:
First Experiments with Neural cvc5. LPAR 2024: 264-277 - [c106]Jan Jakubuv, Mikolás Janota, Josef Urban:
Solving Hard Mizar Problems with Instantiation and Strategy Invention. CICM 2024: 315-333 - [i70]Lasse Blaauwbroek, David M. Cerna, Thibault Gauthier, Jan Jakubuv, Cezary Kaliszyk, Martin Suda, Josef Urban:
Learning Guided Automated Reasoning: A Brief Survey. CoRR abs/2403.04017 (2024) - [i69]Jan Jakubuv, Mikolás Janota, Josef Urban:
Solving Hard Mizar Problems with Instantiation and Strategy Invention. CoRR abs/2406.17762 (2024) - [i68]Jan Jakubuv, Mikolás Janota, Jelle Piepenbrock, Josef Urban:
Machine Learning for Quantifier Selection in cvc5. CoRR abs/2408.14338 (2024) - 2023
- [j25]Thibault Gauthier, Miroslav Olsák, Josef Urban:
Alien coding. Int. J. Approx. Reason. 162: 109009 (2023) - [c105]Thibault Gauthier, Josef Urban:
Learning Program Synthesis for Integer Sequences from Scratch. AAAI 2023: 7670-7677 - [c104]Liao Zhang, Lasse Blaauwbroek, Cezary Kaliszyk, Josef Urban:
Learning Proof Transformations and Its Applications in Interactive Theorem Proving. FroCoS 2023: 236-254 - [c103]Chad E. Brown, Adam Pease, Josef Urban:
Translating SUMO-K to Higher-Order Set Theory. FroCoS 2023: 255-274 - [c102]Mario Carneiro, Chad E. Brown, Josef Urban:
Automated Theorem Proving for Metamath. ITP 2023: 9:1-9:19 - [c101]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: 19:1-19:22 - [c100]Karel Chvalovský, Konstantin Korovin, Jelle Piepenbrock, Josef Urban:
Guiding an Instantiation Prover with Graph Neural Networks. LPAR 2023: 112-123 - [c99]Thibault Gauthier, Chad E. Brown, Mikolas Janota, Josef Urban:
A Mathematical Benchmark for Inductive Theorem Provers. LPAR 2023: 224-237 - [e10]Revantha Ramanayake, Josef Urban:
Automated Reasoning with Analytic Tableaux and Related Methods - 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18-21, 2023, Proceedings. Lecture Notes in Computer Science 14278, Springer 2023, ISBN 978-3-031-43512-6 [contents] - [i67]Thibault Gauthier, Miroslav Olsák, Josef Urban:
Alien Coding. CoRR abs/2301.11479 (2023) - [i66]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 abs/2303.06686 (2023) - [i65]Thibault Gauthier, Chad E. Brown, Mikolas Janota, Josef Urban:
A Mathematical Benchmark for Inductive Theorem Provers. CoRR abs/2304.02986 (2023) - [i64]Chad E. Brown, Adam Pease, Josef Urban:
Translating SUMO-K to Higher-Order Set Theory. CoRR abs/2305.07903 (2023) - 2022
- [c98]Jelle Piepenbrock, Tom Heskes, Mikolás Janota, Josef Urban:
Guiding an Automated Theorem Prover with Neural Rewriting. IJCAR 2022: 597-617 - [c97]Chad E. Brown, Cezary Kaliszyk, Thibault Gauthier, Josef Urban:
Proofgold: Blockchain for Formal Methods. FMBC@CAV 2022: 4:1-4:15 - [c96]Zarathustra Amadeus Goertzel, Jan Jakubuv, Cezary Kaliszyk, Miroslav Olsák, Jelle Piepenbrock, Josef Urban:
The Isabelle ENIGMA. ITP 2022: 16:1-16:21 - [i63]Kimberley Parsons Trommler, Matthias Hafner, Wolfgang Kellerer, Peter Merz, Sigurd Schuster, Josef Urban, Uwe Baeder, Bertram Gunzelmann, Andreas Kornbichler:
Six Questions about 6G. CoRR abs/2201.12266 (2022) - [i62]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 abs/2203.13094 (2022) - [i61]Zarathustra Amadeus Goertzel, Jan Jakubuv, Cezary Kaliszyk, Miroslav Olsák, Jelle Piepenbrock, Josef Urban:
The Isabelle ENIGMA. CoRR abs/2205.01981 (2022) - [i60]Jelle Piepenbrock, Josef Urban, Konstantin Korovin, Miroslav Olsák, Tom Heskes, Mikolas Janota:
Machine Learning Meets The Herbrand Universe. CoRR abs/2210.03590 (2022) - 2021
- [j24]Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, Michael Norrish:
TacticToe: Learning to Prove with Tactics. J. Autom. Reason. 65(2): 257-286 (2021) - [j23]Michael Färber, Cezary Kaliszyk, Josef Urban:
Machine Learning Guidance for Connection Tableaux. J. Autom. Reason. 65(2): 287-320 (2021) - [c95]Zarathustra Amadeus Goertzel, Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban:
Fast and Slow Enigmas and Parental Guidance. FroCoS 2021: 173-191 - [c94]Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Prokop Cerný, Cezary Kaliszyk, Josef Urban:
Online Machine Learning Techniques for Coq: A Comparison. CICM 2021: 67-83 - [c93]Jaroslav Macke, Jirí Sedlár, Miroslav Olsák, Josef Urban, Josef Sivic:
Learning to Solve Geometric Construction Problems from Images. CICM 2021: 167-184 - [c92]Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, Josef Urban:
Towards Finding Longer Proofs. TABLEAUX 2021: 167-186 - [c91]Zsolt Zombori, Josef Urban, Miroslav Olsák:
The Role of Entropy in Guiding a Connection Prover. TABLEAUX 2021: 218-235 - [c90]Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban:
Learning Theorem Proving Components. TABLEAUX 2021: 266-278 - [i59]Jelle Piepenbrock, Tom Heskes, Mikolás Janota, Josef Urban:
Learning Equational Theorem Proving. CoRR abs/2102.05547 (2021) - [i58]Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Prokop Cerný, Cezary Kaliszyk, Josef Urban:
Online Machine Learning Techniques for Coq: A Comparison. CoRR abs/2104.05207 (2021) - [i57]Zsolt Zombori, Josef Urban, Miroslav Olsák:
The Role of Entropy in Guiding a Connection Prover. CoRR abs/2105.14706 (2021) - [i56]Jaroslav Macke, Jirí Sedlár, Miroslav Olsák, Josef Urban, Josef Sivic:
Learning to solve geometric construction problems from images. CoRR abs/2106.14195 (2021) - [i55]Zarathustra Amadeus Goertzel, Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban:
Fast and Slow Enigmas and Parental Guidance. CoRR abs/2107.06750 (2021) - [i54]Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban:
Learning Theorem Proving Components. CoRR abs/2107.10034 (2021) - 2020
- [j22]George Labahn, James H. Davenport, Josef Urban:
Foreword. Math. Comput. Sci. 14(3): 531-532 (2020) - [c89]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: 448-463 - [c88]Zsolt Zombori, Josef Urban, Chad E. Brown:
Prolog Technology Reinforcement Learning Prover - (System Description). IJCAR (2) 2020: 489-507 - [c87]Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, Josef Urban:
Exploration of neural machine translation in autoformalization of mathematics in Mizar. CPP 2020: 85-98 - [c86]Miroslav Olsák, Cezary Kaliszyk, Josef Urban:
Property Invariant Embedding for Automated Reasoning. ECAI 2020: 1395-1402 - [c85]Lasse Blaauwbroek, Josef Urban, Herman Geuvers:
Tactic Learning and Proving for the Coq Proof Assistant. LPAR 2020: 138-150 - [c84]Bartosz Piotrowski, Josef Urban:
Stateful Premise Selection by Recurrent Neural Networks. LPAR 2020: 409-422 - [c83]Lasse Blaauwbroek, Josef Urban, Herman Geuvers:
The Tactician - A Seamless, Interactive Tactic Learner and Prover for Coq. CICM 2020: 271-277 - [c82]Bartosz Piotrowski, Josef Urban:
Guiding Inferences in Connection Tableau by Recurrent Neural Networks. CICM 2020: 309-314 - [c81]Josef Urban, Jan Jakubuv:
First Neural Conjecturing Datasets and Experiments. CICM 2020: 315-323 - [i53]Jan Jakubuv, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, Josef Urban:
ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description). CoRR abs/2002.05406 (2020) - [i52]Lasse Blaauwbroek, Josef Urban, Herman Geuvers:
Tactic Learning and Proving for the Coq Proof Assistant. CoRR abs/2003.09140 (2020) - [i51]Zsolt Zombori, Josef Urban, Chad E. Brown:
Prolog Technology Reinforcement Learning Prover. CoRR abs/2004.06997 (2020) - [i50]Bartosz Piotrowski, Josef Urban:
Stateful Premise Selection by Recurrent Neural Networks. CoRR abs/2004.08212 (2020) - [i49]Josef Urban, Jan Jakubuv:
First Neural Conjecturing Datasets and Experiments. CoRR abs/2005.14664 (2020) - [i48]Lasse Blaauwbroek, Josef Urban, Herman Geuvers:
The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq. CoRR abs/2008.00120 (2020)
2010 – 2019
- 2019
- [c80]Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban:
GRUNGE: A Grand Unified ATP Challenge. CADE 2019: 123-141 - [c79]Karel Chvalovský, Jan Jakubuv, Martin Suda, Josef Urban:
ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E. CADE 2019: 197-215 - [c78]Jan Jakubuv, Josef Urban:
Hammering Mizar by Learning Clause Guidance (Short Paper). ITP 2019: 34:1-34:8 - [c77]Zarathustra Amadeus Goertzel, Jan Jakubuv, Josef Urban:
ENIGMAWatch: ProofWatch Meets ENIGMA. TABLEAUX 2019: 374-388 - [i47]Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban:
GRUNGE: A Grand Unified ATP Challenge. CoRR abs/1903.02539 (2019) - [i46]Karel Chvalovský, Jan Jakubuv, Martin Suda, Josef Urban:
ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E. CoRR abs/1903.03182 (2019) - [i45]Jan Jakubuv, Josef Urban:
Hammering Mizar by Learning Clause Guidance. CoRR abs/1904.01677 (2019) - [i44]Bartosz Piotrowski, Josef Urban:
Guiding Theorem Proving by Recurrent Neural Networks. CoRR abs/1905.07961 (2019) - [i43]Zarathustra Amadeus Goertzel, Jan Jakubuv, Josef Urban:
ENIGMAWatch: ProofWatch Meets ENIGMA. CoRR abs/1905.09565 (2019) - [i42]Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, Josef Urban:
Towards Finding Longer Proofs. CoRR abs/1905.13100 (2019) - [i41]Bartosz Piotrowski, Josef Urban, Chad E. Brown, Cezary Kaliszyk:
Can Neural Networks Learn Symbolic Rewriting? CoRR abs/1911.04873 (2019) - [i40]Miroslav Olsák, Cezary Kaliszyk, Josef Urban:
Property Invariant Embedding for Automated Reasoning. CoRR abs/1911.12073 (2019) - [i39]Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, Josef Urban:
Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar. CoRR abs/1912.02636 (2019) - 2018
- [j21]Pascal Fontaine, Cezary Kaliszyk, Stephan Schulz, Josef Urban:
Foreword to the Special Issue on Automated Reasoning. AI Commun. 31(3): 235-236 (2018) - [j20]Jan Jakubuv, Josef Urban:
Hierarchical invention of theorem proving strategies. AI Commun. 31(3): 237-250 (2018) - [c76]Bartosz Piotrowski, Josef Urban:
ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback. IJCAR 2018: 566-574 - [c75]Zarathustra Amadeus Goertzel, Jan Jakubuv, Stephan Schulz, Josef Urban:
ProofWatch: Watchlist Guidance for Large Theories in E. ITP 2018: 270-288 - [c74]Zarathustra Amadeus Goertzel, Jan Jakubuv, Josef Urban:
ProofWatch Meets ENIGMA: First Experiments. LPAR (Workshop and Short Papers) 2018: 15-22 - [c73]Grzegorz Bancerek, Adam Naumowicz, Josef Urban:
System Description: XSL-Based Translator of Mizar to LaTeX. CICM 2018: 1-6 - [c72]Jan Jakubuv, Josef Urban:
Enhancing ENIGMA Given Clause Guidance. CICM 2018: 118-124 - [c71]Qingxiang Wang, Cezary Kaliszyk, Josef Urban:
First Experiments with Neural Translation of Informal to Formal Mathematics. CICM 2018: 255-270 - [c70]Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Miroslav Olsák:
Reinforcement Learning of Theorem Proving. NeurIPS 2018: 8836-8847 - [e9]Boris Konev, Josef Urban, Philipp Rümmer:
Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning co-located with Federated Logic Conference 2018 (FLoC 2018), Oxford, UK, July 19th, 2018. CEUR Workshop Proceedings 2162, CEUR-WS.org 2018 [contents] - [e8]James H. Davenport, Manuel Kauers, George Labahn, Josef Urban:
Mathematical Software - ICMS 2018 - 6th International Conference, South Bend, IN, USA, July 24-27, 2018, Proceedings. Lecture Notes in Computer Science 10931, Springer 2018, ISBN 978-3-319-96417-1 [contents] - [i38]Bartosz Piotrowski, Josef Urban:
ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback. CoRR abs/1802.03375 (2018) - [i37]Zarathustra Amadeus Goertzel, Jan Jakubuv, Stephan Schulz, Josef Urban:
ProofWatch: Watchlist Guidance for Large Theories in E. CoRR abs/1802.04007 (2018) - [i36]Thibault Gauthier, Cezary Kaliszyk, Josef Urban:
Learning to Reason with HOL4 tactics. CoRR abs/1804.00595 (2018) - [i35]Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, Michael Norrish:
Learning to Prove with Tactics. CoRR abs/1804.00596 (2018) - [i34]Michael Färber, Cezary Kaliszyk, Josef Urban:
Machine Learning Guidance and Proof Certification for Connection Tableaux. CoRR abs/1805.03107 (2018) - [i33]Qingxiang Wang, Cezary Kaliszyk, Josef Urban:
First Experiments with Neural Translation of Informal to Formal Mathematics. CoRR abs/1805.06502 (2018) - [i32]Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Mirek Olsák:
Reinforcement Learning of Theorem Proving. CoRR abs/1805.07563 (2018) - 2017
- [c69]Josef Urban:
AI at CADE/IJCAR. ARCADE@CADE 2017: 33-36 - [c68]Stephan Schulz, Geoff Sutcliffe, Josef Urban, Adam Pease:
Detecting Inconsistencies in Large First-Order Knowledge Bases. CADE 2017: 310-325 - [c67]Michael Färber, Cezary Kaliszyk, Josef Urban:
Monte Carlo Tableau Proof Search. CADE 2017: 563-579 - [c66]Jan Jakubuv, Josef Urban:
BliStrTune: hierarchical invention of theorem proving strategies. CPP 2017: 43-52 - [c65]Jan Jakubuv, Martin Suda, Josef Urban:
Automated Invention of Strategies and Term Orderings for Vampire. GCAI 2017: 121-133 - [c64]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Automating Formalization by Statistical and Semantic Parsing of Mathematics. ITP 2017: 12-27 - [c63]Thibault Gauthier, Cezary Kaliszyk, Josef Urban:
TacticToe: Learning to Reason with HOL4 Tactics. LPAR 2017: 125-143 - [c62]Jan Jakubuv, Josef Urban:
ENIGMA: Efficient Learning-Based Inference Guiding Machine. CICM 2017: 292-302 - [c61]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
System Description: Statistical Parsing of Informalized Mizar Formulas. SYNASC 2017: 169-172 - [i31]Jan Jakubuv, Josef Urban:
ENIGMA: Efficient Learning-based Inference Guiding Machine. CoRR abs/1701.06532 (2017) - 2016
- [j19]Geoff Sutcliffe, Josef Urban:
The CADE-25 Automated Theorem Proving system competition - CASC-25. AI Commun. 29(3): 423-433 (2016) - [j18]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): 219-244 (2016) - [j17]John Harrison, Josef Urban, Freek Wiedijk:
Preface: Twenty Years of the QED Manifesto. J. Formaliz. Reason. 9(1): 1-2 (2016) - [j16]Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, Josef Urban:
Hammering towards QED. J. Formaliz. Reason. 9(1): 101-148 (2016) - [c60]Thibault Gauthier, Cezary Kaliszyk, Josef Urban:
Initial Experiments with Statistical Conjecturing over Large Formal Corpora. FM4M/MathUI/ThEdu/DP/WIP@CIKM 2016: 219-228 - [c59]Cezary Kaliszyk, Karol Pak, Josef Urban:
Towards a mizar environment for isabelle: foundations and language. CPP 2016: 58-65 - [c58]Josef Urban:
Learning Intelligent Theorem Proving from Large Formal Corpora. ISAIM 2016 - [c57]Chad E. Brown, Josef Urban:
Extracting Higher-Order Goals from the Mizar Mathematical Library. CICM 2016: 99-114 - [c56]Jan Jakubuv, Josef Urban:
Extending E Prover with Similarity Based Clause Selection Strategies. CICM 2016: 151-156 - [c55]Geoffrey Irving, Christian Szegedy, Alexander A. Alemi, Niklas Eén, François Chollet, Josef Urban:
DeepMath - Deep Sequence Models for Premise Selection. NIPS 2016: 2235-2243 - [e7]Pascal Fontaine, Stephan Schulz, Josef Urban:
Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning co-located with International Joint Conference on Automated Reasoning (IJCAR 2016), Coimbra, Portugal, July 2nd, 2016. CEUR Workshop Proceedings 1635, CEUR-WS.org 2016 [contents] - [i30]Chad E. Brown, Josef Urban:
Extracting Higher-Order Goals from the Mizar Mathematical Library. CoRR abs/1605.06996 (2016) - [i29]Jan Jakubuv, Josef Urban:
Extending E Prover with Similarity Based Clause Selection Strategies. CoRR abs/1606.03888 (2016) - [i28]Alexander A. Alemi, François Chollet, Geoffrey Irving, Christian Szegedy, Josef Urban:
DeepMath - Deep Sequence Models for Premise Selection. CoRR abs/1606.04442 (2016) - [i27]Michael Färber, Cezary Kaliszyk, Josef Urban:
Monte Carlo Connection Prover. CoRR abs/1611.05990 (2016) - [i26]Jan Jakubuv, Josef Urban:
BliStrTune: Hierarchical Invention of Theorem Proving Strategies. CoRR abs/1611.08733 (2016) - [i25]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Semantic Parsing of Mathematics by Context-based Learning from Aligned Corpora and Theorem Proving. CoRR abs/1611.09703 (2016) - 2015
- [j15]Cezary Kaliszyk, Josef Urban:
Erratum to : Learning-Assisted Automated Reasoning with Flyspeck. J. Autom. Reason. 54(1): 99 (2015) - [j14]Daniel Kühlwein, Josef Urban:
MaLeS: A Framework for Automatic Tuning of Automated Theorem Provers. J. Autom. Reason. 55(2): 91-116 (2015) - [j13]Cezary Kaliszyk, Josef Urban:
MizAR 40 for Mizar 40. J. Autom. Reason. 55(3): 245-256 (2015) - [j12]Cezary Kaliszyk, Josef Urban:
Learning-assisted theorem proving with millions of lemmas. J. Symb. Comput. 69: 109-128 (2015) - [j11]Cezary Kaliszyk, Josef Urban:
HOL(y)Hammer: Online ATP Service for HOL Light. Math. Comput. Sci. 9(1): 5-22 (2015) - [c54]Cezary Kaliszyk, Stephan Schulz, Josef Urban, Jirí Vyskocil:
System Description: E.T. 0.1. CADE 2015: 389-398 - [c53]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Certified Connection Tableaux Proofs for HOL Light and TPTP. CPP 2015: 59-66 - [c52]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Lemmatization for Stronger Reasoning in Large Theories. FroCos 2015: 341-356 - [c51]Josef Urban:
BliStr: The Blind Strategymaker. GCAI 2015: 312-319 - [c50]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Efficient Semantic Features for Automated Reasoning over Large Theories. IJCAI 2015: 3084-3090 - [c49]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Learning to Parse on Aligned Corpora (Rough Diamond). ITP 2015: 227-233 - [c48]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Improving Statistical Linguistic Algorithms for Parsing Mathematics. IWIL@LPAR 2015: 27-36 - [c47]Cezary Kaliszyk, Josef Urban:
FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover. LPAR 2015: 88-96 - [c46]Josef Urban, Robert Veroff:
Experiments with State-of-the-art Automated Provers on Problems in Tarskian Geometry. IWIL@LPAR 2015: 122-126 - [c45]Grzegorz Bancerek, Czeslaw Bylinski, Adam Grabowski, Artur Kornilowicz, Roman Matuszewski, Adam Naumowicz, Karol Pak, Josef Urban:
Mizar: State-of-the-art and Beyond. CICM 2015: 261-279 - [c44]Cezary Kaliszyk, Josef Urban, Umair Siddique, Sanaz Khan Afshar, Cvetan Dunchev, Sofiène Tahar:
Formalizing Physics: Automation, Presentation and Foundation Issues. CICM 2015: 288-295 - [i24]Johan Commelin, Josef Urban:
Auto-hyperlinking the Stacks Project. CICM (Work in Progress) 2015: 19-24 - [i23]Thomas C. Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason M. Rute, Alexey Solovyev, An Hoai Thi Ta, Trung Nam Tran, Diep Thi Trieu, Josef Urban, Ky Khac Vu, Roland Zumkeller:
A formal proof of the Kepler conjecture. CoRR abs/1501.02155 (2015) - 2014
- [j10]Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze, Josef Urban:
Premise Selection for Mathematics by Corpus Analysis and Kernel Methods. J. Autom. Reason. 52(2): 191-213 (2014) - [j9]Cezary Kaliszyk, Josef Urban:
Learning-Assisted Automated Reasoning with Flyspeck. J. Autom. Reason. 53(2): 173-213 (2014) - [c43]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Machine Learner for Automated Reasoning 0.4 and 0.5. PAAR@IJCAR 2014: 60-66 - [c42]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil, Herman Geuvers:
Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description. CICM 2014: 435-439 - [c41]Cezary Kaliszyk, Josef Urban:
Wikis and Collaborative Systems for Large Formal Mathematics. SWCS (LNCS Volume) 2014: 35-52 - [c40]Cezary Kaliszyk, Lionel Mamane, Josef Urban:
Machine Learning of Coq Proof Guidance: First Experiments. SCSS 2014: 27-34 - [c39]Sebastiaan J. C. Joosten, Cezary Kaliszyk, Josef Urban:
Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems. ACL2 2014: 77-85 - [e6]Matthew England, James H. Davenport, Andrea Kohlhase, Michael Kohlhase, Paul Libbrecht, Walther Neuper, Pedro Quaresma, Alan P. Sexton, Petr Sojka, Josef Urban, Stephen M. Watt:
Joint Proceedings of the MathUI, OpenMath and ThEdu Workshops and Work in Progress track at CICM co-located with Conferences on Intelligent Computer Mathematics (CICM 2014), Coimbra, Portugal, July 7-11, 2014. CEUR Workshop Proceedings 1186, CEUR-WS.org 2014 [contents] - [e5]Stephen M. Watt, James H. Davenport, Alan P. Sexton, Petr Sojka, Josef Urban:
Intelligent Computer Mathematics - International Conference, CICM 2014, Coimbra, Portugal, July 7-11, 2014. Proceedings. Lecture Notes in Computer Science 8543, Springer 2014, ISBN 978-3-319-08433-6 [contents] - [r1]John Harrison, Josef Urban, Freek Wiedijk:
History of Interactive Theorem Proving. Computational Logic 2014: 135-214 - [i22]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Machine Learner for Automated Reasoning 0.4 and 0.5. CoRR abs/1402.2359 (2014) - [i21]Cezary Kaliszyk, Josef Urban:
Learning-assisted Theorem Proving with Millions of Lemmas. CoRR abs/1402.3578 (2014) - [i20]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil, Herman Geuvers:
Developing Corpus-based Translation Methods between Informal and Formal Mathematics: Project Description. CoRR abs/1405.3451 (2014) - [i19]Cezary Kaliszyk, Lionel Mamane, Josef Urban:
Machine Learning of Coq Proof Guidance: First Experiments. CoRR abs/1410.5467 (2014) - [i18]Cezary Kaliszyk, Josef Urban, Jirí Vyskocil:
Certified Connection Tableaux Proofs for HOL Light and TPTP. CoRR abs/1410.5476 (2014) - 2013
- [j8]Mihnea Iancu, Michael Kohlhase, Florian Rabe, Josef Urban:
The Mizar Mathematical Library in OMDoc: Translation and Applications. J. Autom. Reason. 50(2): 191-202 (2013) - [j7]Josef Urban, Piotr Rudnicki, Geoff Sutcliffe:
ATP and Presentation Service for Mizar Formalizations. J. Autom. Reason. 50(2): 229-241 (2013) - [c38]Josef Urban, Jirí Vyskocil:
Theorem Proving in Large Formal Mathematics as an Emerging AI Field. Automated Reasoning and Mathematics 2013: 240-257 - [c37]Cezary Kaliszyk, Josef Urban:
Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution. PxTP@CADE 2013: 87-95 - [c36]Cezary Kaliszyk, Josef Urban:
PRocH: Proof Reconstruction for HOL Light. CADE 2013: 267-274 - [c35]Daniel Kühlwein, Stephan Schulz, Josef Urban:
E-MaLeS 1.1. CADE 2013: 407-413 - [c34]Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, Josef Urban:
MaSh: Machine Learning for Sledgehammer. ITP 2013: 35-50 - [c33]Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers:
Communicating Formal Proofs: The Case of Flyspeck. ITP 2013: 451-456 - [c32]Cezary Kaliszyk, Josef Urban:
Lemma Mining over HOL Light. LPAR 2013: 503-517 - [c31]Cezary Kaliszyk, Josef Urban:
Automated Reasoning Service for HOL Light. MKM/Calculemus/DML 2013: 120-135 - [c30]Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers:
Formal Mathematics on Display: A Wiki for Flyspeck. MKM/Calculemus/DML 2013: 152-167 - [e4]Jasmin Christian Blanchette, Josef Urban:
Third International Workshop on Proof Exchange for Theorem Proving, PxTP 2013, Lake Placid, NY, USA, June 9-10, 2013. EPiC Series in Computing 14, EasyChair 2013 [contents] - [i17]Josef Urban:
BliStr: The Blind Strategymaker. CoRR abs/1301.2683 (2013) - [i16]Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers:
Formal Mathematics on Display: A Wiki for Flyspeck. CoRR abs/1305.5710 (2013) - [i15]Daniel Kühlwein, Josef Urban:
MaLeS: A Framework for Automatic Tuning of Automated Theorem Provers. CoRR abs/1308.2116 (2013) - [i14]Cezary Kaliszyk, Josef Urban:
HOL(y)Hammer: Online ATP Service for HOL Light. CoRR abs/1309.4962 (2013) - [i13]Cezary Kaliszyk, Josef Urban:
Lemma Mining over HOL Light. CoRR abs/1310.2797 (2013) - [i12]Cezary Kaliszyk, Josef Urban:
MizAR 40 for Mizar 40. CoRR abs/1310.2805 (2013) - 2012
- [c29]Jesse Alama, Lionel Mamane, Josef Urban:
Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar. AISC/MKM/Calculemus 2012: 1-16 - [c28]Carst Tankink, Christoph Lange, Josef Urban:
Point-and-Write - Documenting Formal Mathematics by Reference. AISC/MKM/Calculemus 2012: 169-185 - [c27]Cezary Kaliszyk, Josef Urban:
Initial Experiments with External Provers and Premise Selection on HOL Light Corpora. PAAR@IJCAR 2012: 72-81 - [c26]Daniel Kühlwein, Josef Urban:
Learning from Multiple Proofs: First Experiments. PAAR@IJCAR 2012: 82-94 - [c25]Daniel Kühlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban, Tom Heskes:
Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics. IJCAR 2012: 378-392 - [c24]Jesse Alama, Daniel Kühlwein, Josef Urban:
Automated and Human Proofs in General Mathematics: An Initial Comparison. LPAR 2012: 37-45 - [i11]Carst Tankink, Christoph Lange, Josef Urban:
Point-and-write --- Documenting Formal Mathematics by Reference. CoRR abs/1204.5094 (2012) - [i10]Josef Urban:
Parallelizing Mizar. CoRR abs/1206.0141 (2012) - [i9]Josef Urban, Jirí Vyskocil:
Theorem Proving in Large Formal Mathematics as an Emerging AI Field. CoRR abs/1209.3914 (2012) - [i8]Cezary Kaliszyk, Josef Urban:
Learning-assisted Automated Reasoning with Flyspeck. CoRR abs/1211.7012 (2012) - 2011
- [c23]Josef Urban:
An Overview of Methods for Large-Theory Automated Theorem Proving. ATE 2011: 3-8 - [c22]Daniel Kühlwein, Josef Urban, Evgeni Tsivtsivadze, Herman Geuvers, Tom Heskes:
Multi-output Ranking for Automated Reasoning. KDIR 2011: 42-51 - [c21]Josef Urban:
Content-based encoding of mathematical and code libraries. MathWikis@ITP 2011: 49-53 - [c20]Jesse Alama, Kasper Brink, Lionel Mamane, Josef Urban:
Large Formal Wikis: Issues and Solutions. Calculemus/MKM 2011: 133-148 - [c19]Jesse Alama, Michael Kohlhase, Lionel Mamane, Adam Naumowicz, Piotr Rudnicki, Josef Urban:
Licensing the Mizar Mathematical Library. Calculemus/MKM 2011: 149-163 - [c18]Daniel Kühlwein, Josef Urban, Evgeni Tsivtsivadze, Herman Geuvers, Tom Heskes:
Learning2Reason. Calculemus/MKM 2011: 298-300 - [c17]Piotr Rudnicki, Josef Urban:
Escape to ATP for Mizar. PxTP 2011: 46-59 - [c16]Evgeni Tsivtsivadze, Josef Urban, Herman Geuvers, Tom Heskes:
Semantic Graph Kernels for Automated Reasoning. SDM 2011: 795-803 - [c15]Josef Urban, Jirí Vyskocil, Petr Stepánek:
MaLeCoP Machine Learning Connection Prover. TABLEAUX 2011: 263-277 - [e3]Christoph Lange, Josef Urban:
Proceedings of the ITP 2011 Workshop on Mathematical Wikis, Nijmegen, The Netherlands, August 27th, 2011. CEUR Workshop Proceedings 767, CEUR-WS.org 2011 [contents] - [e2]James H. Davenport, William M. Farmer, Josef Urban, Florian Rabe:
Intelligent Computer Mathematics - 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011. Proceedings. Lecture Notes in Computer Science 6824, Springer 2011, ISBN 978-3-642-22672-4 [contents] - [i7]Jesse Alama, Kasper Brink, Lionel Mamane, Josef Urban:
Large Formal Wikis: Issues and Solutions. CoRR abs/1107.3209 (2011) - [i6]Jesse Alama, Michael Kohlhase, Adam Naumowicz, Piotr Rudnicki, Josef Urban, Lionel Mamane:
Licensing the Mizar Mathematical Library. CoRR abs/1107.3212 (2011) - [i5]Jesse Alama, Daniel Kühlwein, Evgeni Tsivtsivadze, Josef Urban, Tom Heskes:
Premise Selection for Mathematics by Corpus Analysis and Kernel Methods. CoRR abs/1108.3446 (2011) - [i4]Josef Urban, Piotr Rudnicki, Geoff Sutcliffe:
ATP and Presentation Service for Mizar Formalizations. CoRR abs/1109.0616 (2011) - [i3]Jesse Alama, Lionel Mamane, Josef Urban:
Dependencies in Formal Mathematics. CoRR abs/1109.3687 (2011) - 2010
- [c14]Josef Urban, Geoff Sutcliffe:
Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar. AISC/MKM/Calculemus 2010: 132-146 - [c13]Josef Urban, Jesse Alama, Piotr Rudnicki, Herman Geuvers:
A Wiki for Mizar: Motivation, Considerations, and Initial Prototype. AISC/MKM/Calculemus 2010: 455-469 - [c12]Josef Urban, Krystof Hoder, Andrei Voronkov:
Evaluation of Automated Theorem Proving on the Mizar Mathematical Library. ICMS 2010: 155-166 - [c11]Jirí Vyskocil, David Stanovský, Josef Urban:
Automated Proof Compression by Invention of New Definitions. LPAR (Dakar) 2010: 447-462 - [i2]Josef Urban, Jesse Alama, Piotr Rudnicki, Herman Geuvers:
A Wiki for Mizar: Motivation, Considerations, and Initial Prototype. CoRR abs/1005.4552 (2010) - [i1]Josef Urban, Geoff Sutcliffe:
Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar. CoRR abs/1005.4592 (2010)
2000 – 2009
- 2008
- [j6]Josef Urban, Geoff Sutcliffe:
ATP-based Cross-Verification of Mizar Proofs: Method, Systems, and First Experiments. Math. Comput. Sci. 2(2): 231-251 (2008) - [c10]Josef Urban, Geoff Sutcliffe, Petr Pudlák, Jirí Vyskocil:
MaLARea SG1- Machine Learner for Automated Reasoning with Semantic Guidance. IJCAR 2008: 441-456 - [c9]Josef Urban:
Automated Reasoning for Mizar: Artificial Intelligence through Knowledge Exchange. LPAR Workshops 2008 - 2007
- [c8]Josef Urban:
MaLARea: a Metasystem for Automated Reasoning in Large Theories. ESARLT 2007 - [c7]Josef Urban, Geoff Sutcliffe:
ATP Cross-Verification of the Mizar MPTP Challenge Problems. LPAR 2007: 546-560 - [e1]Geoff Sutcliffe, Josef Urban, Stephan Schulz:
Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, Bremen, Germany, 17th July 2007. CEUR Workshop Proceedings 257, CEUR-WS.org 2007 [contents] - 2006
- [j5]Josef Urban:
Momm - Fast Interreduction and Retrieval in Large Libraries of Formalized Mathematics. Int. J. Artif. Intell. Tools 15(1): 109-130 (2006) - [j4]Josef Urban:
MizarMode - an integrated proof assistance tool for the Mizar way of formalizing mathematics. J. Appl. Log. 4(4): 414-427 (2006) - [j3]Josef Urban:
MPTP 0.2: Design, Implementation, and Initial Experiments. J. Autom. Reason. 37(1-2): 21-43 (2006) - [c6]Josef Urban, Grzegorz Bancerek:
Presenting and Explaining Mizar. UITP@FLoC 2006: 63-74 - 2005
- [c5]Josef Urban:
XML-izing Mizar: Making Semantic Processing and Presentation of MML Easy. MKM 2005: 346-360 - 2004
- [j2]Josef Urban:
MPTP - Motivation, Implementation, First Experiments. J. Autom. Reason. 33(3-4): 319-339 (2004) - [c4]Grzegorz Bancerek, Josef Urban:
Integrated Semantic Browsing of the Mizar Mathematical Library for Authoring Mizar Articles. MKM 2004: 44-57 - 2003
- [c3]Josef Urban:
Translating Mizar for First Order Theorem Provers. MKM 2003: 203-215 - [c2]Josef Urban:
MPTP 0.1: System Description. FTP 2003: 147-152 - 2001
- [j1]Josef Urban, Dave Wisely, Edgar Bolinth, Georg Neureiter, Mika Liljeberg, Tomás Robles Valladares:
BRAIN - an architecture for a broadband radio access network of the next generation. Wirel. Commun. Mob. Comput. 1(1): 55-75 (2001) - 2000
- [c1]Dave Wisely, Werner Mohr, Josef Urban:
Broadband Radio Access for IP-based networks (BRAIN)-a key enabler for mobile Internet access. PIMRC 2000: 431-436
Coauthor Index
Mikolás Janota
aka: Mikolas Janota
aka: Mikolas Janota
[c109] [i70] [c104] [c101] [i66] [c97] [c96] [i61] [j24] [j23] [c94] [c92] [i58] [c87] [c86] [c80] [i47] [i42] [i41] [i40] [i39] [j21] [c71] [c70] [i36] [i35] [i34] [i33] [i32] [c67] [c64] [c63] [c61] [j18] [j16] [c60] [c59] [i27] [i25] [j15] [j13] [j12] [j11] [c54] [c53] [c52] [c50] [c49] [c48] [c47] [c44] [i23] [j9] [c43] [c42] [c41] [c40] [c39] [i22] [i21] [i20] [i19] [i18] [c37] [c36] [c34] [c33] [c32] [c31] [c30] [i16] [i14] [i13] [i12] [c27] [i8]
Miroslav Olsák
aka: Mirek Olsák
aka: Mirek Olsák
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2025-01-20 22:58 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
