Josef Urban - RankMe

228 papers A* 3A 15B 31C 18Misc 2Journal 102Unranked 48

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone? CoRR Josef Urban
2026	J	`jnl`	Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents. CoRR Chad E. Brown, Cezary Kaliszyk, Josef Urban
2026	J	`jnl`	Machine learning for quantifier selection in cvc5. Int. J. Approx. Reason. Jan Jakubuv, Mikolás Janota, Jelle Piepenbrock, Josef Urban
2025	C	`conf`	Exploring Formal Math on the Blockchain: An Explorer for Proofgold. CICM Chad E. Brown, Cezary Kaliszyk, Josef Urban
2025	J	`jnl`	Exploring Formal Math on the Blockchain: An Explorer for Proofgold. CoRR Chad E. Brown, Cezary Kaliszyk, Josef Urban
2025	C	`conf`	Hammering Higher Order Set Theory. CICM Chad E. Brown, Cezary Kaliszyk, Martin Suda, Josef Urban
2025	J	`jnl`	Hammering Higher Order Set Theory. CoRR Chad E. Brown, Cezary Kaliszyk, Martin Suda, Josef Urban
2025	J	`jnl`	Invariant neural architecture for learning term synthesis in instantiation proving. J. Symb. Comput. Jelle Piepenbrock, Josef Urban, Konstantin Korovin, Miroslav Olsák, Tom Heskes, Mikolás Janota
2025	A	`conf`	Learning Conjecturing from Scratch. CADE Thibault Gauthier, Josef Urban
2025	J	`jnl`	Learning Conjecturing from Scratch. CoRR Thibault Gauthier, Josef Urban
2025	—	`conf`	Payment Channels with Proofs. BCCA Chad E. Brown, Cezary Kaliszyk, Josef Urban
2025	J	`jnl`	Payment Channels with Proofs. CoRR Chad E. Brown, Cezary Kaliszyk, Josef Urban
2024	B	`conf`	First Experiments with Neural cvc5. LPAR Jelle Piepenbrock, Mikolas Janota, Josef Urban, Jan Jakubuv
2024	—	`conf`	Learning Guided Automated Reasoning: A Brief Survey. Logics and Type Systems in Theory and Practice Lasse Blaauwbroek, David M. Cerna, Thibault Gauthier, Jan Jakubuv, Cezary Kaliszyk, Martin Suda, Josef Urban
2024	J	`jnl`	Learning Guided Automated Reasoning: A Brief Survey. CoRR Lasse Blaauwbroek, David M. Cerna, Thibault Gauthier, Jan Jakubuv, Cezary Kaliszyk, Martin Suda, Josef Urban
2024	A	`conf`	Machine Learning for Quantifier Selection in cvc5. ECAI Jan Jakubuv, Mikolás Janota, Jelle Piepenbrock, Josef Urban
2024	J	`jnl`	Machine Learning for Quantifier Selection in cvc5. CoRR Jan Jakubuv, Mikolás Janota, Jelle Piepenbrock, Josef Urban
2024	C	`conf`	Solving Hard Mizar Problems with Instantiation and Strategy Invention. CICM Jan Jakubuv, Mikolás Janota, Josef Urban
2024	J	`jnl`	Solving Hard Mizar Problems with Instantiation and Strategy Invention. CoRR Jan Jakubuv, Mikolás Janota, Josef Urban
2024	B	`conf`	Some Adventures in Learning Proving, Instantiation and Synthesis. FMCAD Josef Urban
2023	B	`conf`	A Mathematical Benchmark for Inductive Theorem Provers. LPAR Thibault Gauthier, Chad E. Brown, Mikolas Janota, Josef Urban
2023	J	`jnl`	A Mathematical Benchmark for Inductive Theorem Provers. CoRR Thibault Gauthier, Chad E. Brown, Mikolas Janota, Josef Urban
2023	J	`jnl`	Alien Coding. CoRR Thibault Gauthier, Miroslav Olsák, Josef Urban
2023	J	`jnl`	Alien coding. Int. J. Approx. Reason. Thibault Gauthier, Miroslav Olsák, Josef Urban
2023	B	`ed.`	Automated Reasoning with Analytic Tableaux and Related Methods - 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18-21, 2023, Proceedings TABLEAUX Revantha Ramanayake, Josef Urban
2023	B	`conf`	Automated Theorem Proving for Metamath. ITP Mario Carneiro, Chad E. Brown, Josef Urban
2023	B	`conf`	Guiding an Instantiation Prover with Graph Neural Networks. LPAR Karel Chvalovský, Konstantin Korovin, Jelle Piepenbrock, Josef Urban
2023	A*	`conf`	Learning Program Synthesis for Integer Sequences from Scratch. AAAI Thibault Gauthier, Josef Urban
2023	—	`conf`	Learning Proof Transformations and Its Applications in Interactive Theorem Proving. FroCoS Liao Zhang, Lasse Blaauwbroek, Cezary Kaliszyk, Josef Urban
2023	B	`conf`	MizAR 60 for Mizar 50. ITP Jan Jakubuv, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban
2023	J	`jnl`	MizAR 60 for Mizar 50. CoRR Jan Jakubuv, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban
2023	—	`conf`	Translating SUMO-K to Higher-Order Set Theory. FroCoS Chad E. Brown, Adam Pease, Josef Urban
2023	J	`jnl`	Translating SUMO-K to Higher-Order Set Theory. CoRR Chad E. Brown, Adam Pease, Josef Urban
2022	A	`conf`	Guiding an Automated Theorem Prover with Neural Rewriting. IJCAR Jelle Piepenbrock, Tom Heskes, Mikolás Janota, Josef Urban
2022	J	`jnl`	Machine Learning Meets The Herbrand Universe. CoRR Jelle Piepenbrock, Josef Urban, Konstantin Korovin, Miroslav Olsák, Tom Heskes, Mikolas Janota
2022	J	`jnl`	PREVIEW VERSION: Six Insights into 6G: Orientation and Input for Developing Your Strategic 6G Research Plan. CoRR Kimberley Parsons Trommler, Matthias Hafner, Wolfgang Kellerer, Peter Merz, Sigurd Schuster, Josef Urban, Uwe Baeder, Bertram Gunzelmann, Andreas Kornbichler
2022	—	`conf`	Proofgold: Blockchain for Formal Methods. FMBC@CAV Chad E. Brown, Cezary Kaliszyk, Thibault Gauthier, Josef Urban
2022	J	`jnl`	Six Questions about 6G. CoRR Kimberley Parsons Trommler, Matthias Hafner, Wolfgang Kellerer, Peter Merz, Sigurd Schuster, Josef Urban, Uwe Baeder, Bertram Gunzelmann, Andreas Kornbichler
2022	B	`conf`	The Isabelle ENIGMA. ITP Zarathustra Amadeus Goertzel, Jan Jakubuv, Cezary Kaliszyk, Miroslav Olsák, Jelle Piepenbrock, Josef Urban
2022	J	`jnl`	The Isabelle ENIGMA. CoRR Zarathustra Amadeus Goertzel, Jan Jakubuv, Cezary Kaliszyk, Miroslav Olsák, Jelle Piepenbrock, Josef Urban
2021	—	`conf`	Fast and Slow Enigmas and Parental Guidance. FroCoS Zarathustra Amadeus Goertzel, Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban
2021	J	`jnl`	Fast and Slow Enigmas and Parental Guidance. CoRR Zarathustra Amadeus Goertzel, Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban
2021	J	`jnl`	Learning Equational Theorem Proving. CoRR Jelle Piepenbrock, Tom Heskes, Mikolás Janota, Josef Urban
2021	B	`conf`	Learning Theorem Proving Components. TABLEAUX Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban
2021	J	`jnl`	Learning Theorem Proving Components. CoRR Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban
2021	C	`conf`	Learning to Solve Geometric Construction Problems from Images. CICM Jaroslav Macke, Jirí Sedlár, Miroslav Olsák, Josef Urban, Josef Sivic
2021	J	`jnl`	Learning to solve geometric construction problems from images. CoRR Jaroslav Macke, Jirí Sedlár, Miroslav Olsák, Josef Urban, Josef Sivic
2021	J	`jnl`	Machine Learning Guidance for Connection Tableaux. J. Autom. Reason. Michael Färber, Cezary Kaliszyk, Josef Urban
2021	C	`conf`	Online Machine Learning Techniques for Coq: A Comparison. CICM Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Prokop Cerný, Cezary Kaliszyk, Josef Urban
2021	J	`jnl`	Online Machine Learning Techniques for Coq: A Comparison. CoRR Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Prokop Cerný, Cezary Kaliszyk, Josef Urban
2021	J	`jnl`	TacticToe: Learning to Prove with Tactics. J. Autom. Reason. Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, Michael Norrish
2021	B	`conf`	The Role of Entropy in Guiding a Connection Prover. TABLEAUX Zsolt Zombori, Josef Urban, Miroslav Olsák
2021	J	`jnl`	The Role of Entropy in Guiding a Connection Prover. CoRR Zsolt Zombori, Josef Urban, Miroslav Olsák
2021	B	`conf`	Towards Finding Longer Proofs. TABLEAUX Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, Josef Urban
2020	—	`conf`	ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description). IJCAR (2) Jan Jakubuv, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, Josef Urban
2020	J	`jnl`	ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description). CoRR Jan Jakubuv, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, Josef Urban
2020	B	`conf`	Exploration of neural machine translation in autoformalization of mathematics in Mizar. CPP Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, Josef Urban
2020	C	`conf`	First Neural Conjecturing Datasets and Experiments. CICM Josef Urban, Jan Jakubuv
2020	J	`jnl`	First Neural Conjecturing Datasets and Experiments. CoRR Josef Urban, Jan Jakubuv
2020	J	`jnl`	Foreword. Math. Comput. Sci. George Labahn, James H. Davenport, Josef Urban
2020	C	`conf`	Guiding Inferences in Connection Tableau by Recurrent Neural Networks. CICM Bartosz Piotrowski, Josef Urban
2020	—	`conf`	Prolog Technology Reinforcement Learning Prover - (System Description). IJCAR (2) Zsolt Zombori, Josef Urban, Chad E. Brown
2020	J	`jnl`	Prolog Technology Reinforcement Learning Prover. CoRR Zsolt Zombori, Josef Urban, Chad E. Brown
2020	A	`conf`	Property Invariant Embedding for Automated Reasoning. ECAI Miroslav Olsák, Cezary Kaliszyk, Josef Urban
2020	B	`conf`	Stateful Premise Selection by Recurrent Neural Networks. LPAR Bartosz Piotrowski, Josef Urban
2020	J	`jnl`	Stateful Premise Selection by Recurrent Neural Networks. CoRR Bartosz Piotrowski, Josef Urban
2020	B	`conf`	Tactic Learning and Proving for the Coq Proof Assistant. LPAR Lasse Blaauwbroek, Josef Urban, Herman Geuvers
2020	J	`jnl`	Tactic Learning and Proving for the Coq Proof Assistant. CoRR Lasse Blaauwbroek, Josef Urban, Herman Geuvers
2020	J	`jnl`	The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq. CoRR Lasse Blaauwbroek, Josef Urban, Herman Geuvers
2020	C	`conf`	The Tactician - A Seamless, Interactive Tactic Learner and Prover for Coq. CICM Lasse Blaauwbroek, Josef Urban, Herman Geuvers
2019	J	`jnl`	Can Neural Networks Learn Symbolic Rewriting? CoRR Bartosz Piotrowski, Josef Urban, Chad E. Brown, Cezary Kaliszyk
2019	A	`conf`	ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E. CADE Karel Chvalovský, Jan Jakubuv, Martin Suda, Josef Urban
2019	J	`jnl`	ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E. CoRR Karel Chvalovský, Jan Jakubuv, Martin Suda, Josef Urban
2019	B	`conf`	ENIGMAWatch: ProofWatch Meets ENIGMA. TABLEAUX Zarathustra Amadeus Goertzel, Jan Jakubuv, Josef Urban
2019	J	`jnl`	ENIGMAWatch: ProofWatch Meets ENIGMA. CoRR Zarathustra Amadeus Goertzel, Jan Jakubuv, Josef Urban
2019	J	`jnl`	Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar. CoRR Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, Josef Urban
2019	A	`conf`	GRUNGE: A Grand Unified ATP Challenge. CADE Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban
2019	J	`jnl`	GRUNGE: A Grand Unified ATP Challenge. CoRR Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban
2019	J	`jnl`	Guiding Theorem Proving by Recurrent Neural Networks. CoRR Bartosz Piotrowski, Josef Urban
2019	B	`conf`	Hammering Mizar by Learning Clause Guidance (Short Paper). ITP Jan Jakubuv, Josef Urban
2019	J	`jnl`	Hammering Mizar by Learning Clause Guidance. CoRR Jan Jakubuv, Josef Urban
2019	J	`jnl`	Property Invariant Embedding for Automated Reasoning. CoRR Miroslav Olsák, Cezary Kaliszyk, Josef Urban
2019	J	`jnl`	Towards Finding Longer Proofs. CoRR Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, Josef Urban
2018	A	`conf`	ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback. IJCAR Bartosz Piotrowski, Josef Urban
2018	J	`jnl`	ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback. CoRR Bartosz Piotrowski, Josef Urban
2018	C	`conf`	Enhancing ENIGMA Given Clause Guidance. CICM Jan Jakubuv, Josef Urban
2018	C	`conf`	First Experiments with Neural Translation of Informal to Formal Mathematics. CICM Qingxiang Wang, Cezary Kaliszyk, Josef Urban
2018	J	`jnl`	First Experiments with Neural Translation of Informal to Formal Mathematics. CoRR Qingxiang Wang, Cezary Kaliszyk, Josef Urban
2018	J	`jnl`	Foreword to the Special Issue on Automated Reasoning. AI Commun. Pascal Fontaine, Cezary Kaliszyk, Stephan Schulz, Josef Urban
2018	J	`jnl`	Hierarchical invention of theorem proving strategies. AI Commun. Jan Jakubuv, Josef Urban
2018	J	`jnl`	Learning to Prove with Tactics. CoRR Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, Michael Norrish
2018	J	`jnl`	Learning to Reason with HOL4 tactics. CoRR Thibault Gauthier, Cezary Kaliszyk, Josef Urban
2018	J	`jnl`	Machine Learning Guidance and Proof Certification for Connection Tableaux. CoRR Michael Färber, Cezary Kaliszyk, Josef Urban
2018	—	`ed.`	Mathematical Software - ICMS 2018 - 6th International Conference, South Bend, IN, USA, July 24-27, 2018, Proceedings ICMS James H. Davenport, Manuel Kauers, George Labahn, Josef Urban
2018	—	`ed.`	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. PAAR@FLoC Boris Konev, Josef Urban, Philipp Rümmer
2018	—	`conf`	ProofWatch Meets ENIGMA: First Experiments. LPAR (Workshop and Short Papers) Zarathustra Amadeus Goertzel, Jan Jakubuv, Josef Urban
2018	B	`conf`	ProofWatch: Watchlist Guidance for Large Theories in E. ITP Zarathustra Amadeus Goertzel, Jan Jakubuv, Stephan Schulz, Josef Urban
2018	J	`jnl`	ProofWatch: Watchlist Guidance for Large Theories in E. CoRR Zarathustra Amadeus Goertzel, Jan Jakubuv, Stephan Schulz, Josef Urban
2018	A*	`conf`	Reinforcement Learning of Theorem Proving. NeurIPS Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Miroslav Olsák
2018	J	`jnl`	Reinforcement Learning of Theorem Proving. CoRR Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Mirek Olsák
2018	C	`conf`	System Description: XSL-Based Translator of Mizar to LaTeX. CICM Grzegorz Bancerek, Adam Naumowicz, Josef Urban
2017	—	`conf`	AI at CADE/IJCAR. ARCADE@CADE Josef Urban
2017	—	`conf`	Automated Invention of Strategies and Term Orderings for Vampire. GCAI Jan Jakubuv, Martin Suda, Josef Urban
2017	B	`conf`	Automating Formalization by Statistical and Semantic Parsing of Mathematics. ITP Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
2017	B	`conf`	BliStrTune: hierarchical invention of theorem proving strategies. CPP Jan Jakubuv, Josef Urban
2017	A	`conf`	Detecting Inconsistencies in Large First-Order Knowledge Bases. CADE Stephan Schulz, Geoff Sutcliffe, Josef Urban, Adam Pease
2017	C	`conf`	ENIGMA: Efficient Learning-Based Inference Guiding Machine. CICM Jan Jakubuv, Josef Urban
2017	J	`jnl`	ENIGMA: Efficient Learning-based Inference Guiding Machine. CoRR Jan Jakubuv, Josef Urban
2017	A	`conf`	Monte Carlo Tableau Proof Search. CADE Michael Färber, Cezary Kaliszyk, Josef Urban
2017	Misc	`conf`	System Description: Statistical Parsing of Informalized Mizar Formulas. SYNASC Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
2017	B	`conf`	TacticToe: Learning to Reason with HOL4 Tactics. LPAR Thibault Gauthier, Cezary Kaliszyk, Josef Urban
2016	J	`jnl`	A Learning-Based Fact Selector for Isabelle/HOL. J. Autom. Reason. Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, Josef Urban
2016	J	`jnl`	BliStrTune: Hierarchical Invention of Theorem Proving Strategies. CoRR Jan Jakubuv, Josef Urban
2016	—	`conf`	DeepMath - Deep Sequence Models for Premise Selection. NIPS Geoffrey Irving, Christian Szegedy, Alexander A. Alemi, Niklas Eén, François Chollet, Josef Urban
2016	J	`jnl`	DeepMath - Deep Sequence Models for Premise Selection. CoRR Alexander A. Alemi, François Chollet, Geoffrey Irving, Christian Szegedy, Josef Urban
2016	C	`conf`	Extending E Prover with Similarity Based Clause Selection Strategies. CICM Jan Jakubuv, Josef Urban
2016	J	`jnl`	Extending E Prover with Similarity Based Clause Selection Strategies. CoRR Jan Jakubuv, Josef Urban
2016	C	`conf`	Extracting Higher-Order Goals from the Mizar Mathematical Library. CICM Chad E. Brown, Josef Urban
2016	J	`jnl`	Extracting Higher-Order Goals from the Mizar Mathematical Library. CoRR Chad E. Brown, Josef Urban
2016	J	`jnl`	Hammering towards QED. J. Formaliz. Reason. Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, Josef Urban
2016	—	`conf`	Initial Experiments with Statistical Conjecturing over Large Formal Corpora. FM4M/MathUI/ThEdu/DP/WIP@CIKM Thibault Gauthier, Cezary Kaliszyk, Josef Urban
2016	Misc	`conf`	Learning Intelligent Theorem Proving from Large Formal Corpora. ISAIM Josef Urban
2016	J	`jnl`	Monte Carlo Connection Prover. CoRR Michael Färber, Cezary Kaliszyk, Josef Urban
2016	J	`jnl`	Preface: Twenty Years of the QED Manifesto. J. Formaliz. Reason. John Harrison, Josef Urban, Freek Wiedijk
2016	—	`ed.`	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. PAAR@IJCAR Pascal Fontaine, Stephan Schulz, Josef Urban
2016	J	`jnl`	Semantic Parsing of Mathematics by Context-based Learning from Aligned Corpora and Theorem Proving. CoRR Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
2016	J	`jnl`	The CADE-25 Automated Theorem Proving system competition - CASC-25. AI Commun. Geoff Sutcliffe, Josef Urban
2016	B	`conf`	Towards a mizar environment for isabelle: foundations and language. CPP Cezary Kaliszyk, Karol Pak, Josef Urban
2015	J	`jnl`	A formal proof of the Kepler conjecture. CoRR 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
2015	—	`conf`	Auto-hyperlinking the Stacks Project. CICM (Work in Progress) Johan Commelin, Josef Urban
2015	—	`conf`	BliStr: The Blind Strategymaker. GCAI Josef Urban
2015	B	`conf`	Certified Connection Tableaux Proofs for HOL Light and TPTP. CPP Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
2015	A*	`conf`	Efficient Semantic Features for Automated Reasoning over Large Theories. IJCAI Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
2015	J	`jnl`	Erratum to : Learning-Assisted Automated Reasoning with Flyspeck. J. Autom. Reason. Cezary Kaliszyk, Josef Urban
2015	—	`conf`	Experiments with State-of-the-art Automated Provers on Problems in Tarskian Geometry. IWIL@LPAR Josef Urban, Robert Veroff
2015	B	`conf`	FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover. LPAR Cezary Kaliszyk, Josef Urban
2015	C	`conf`	Formalizing Physics: Automation, Presentation and Foundation Issues. CICM Cezary Kaliszyk, Josef Urban, Umair Siddique, Sanaz Khan Afshar, Cvetan Dunchev, Sofiène Tahar
2015	J	`jnl`	HOL(y)Hammer: Online ATP Service for HOL Light. Math. Comput. Sci. Cezary Kaliszyk, Josef Urban
2015	—	`conf`	Improving Statistical Linguistic Algorithms for Parsing Mathematics. IWIL@LPAR Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
2015	B	`conf`	Learning to Parse on Aligned Corpora (Rough Diamond). ITP Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
2015	J	`jnl`	Learning-assisted theorem proving with millions of lemmas. J. Symb. Comput. Cezary Kaliszyk, Josef Urban
2015	—	`conf`	Lemmatization for Stronger Reasoning in Large Theories. FroCos Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
2015	J	`jnl`	MaLeS: A Framework for Automatic Tuning of Automated Theorem Provers. J. Autom. Reason. Daniel Kühlwein, Josef Urban
2015	J	`jnl`	MizAR 40 for Mizar 40. J. Autom. Reason. Cezary Kaliszyk, Josef Urban
2015	C	`conf`	Mizar: State-of-the-art and Beyond. CICM Grzegorz Bancerek, Czeslaw Bylinski, Adam Grabowski, Artur Kornilowicz, Roman Matuszewski, Adam Naumowicz, Karol Pak, Josef Urban
2015	A	`conf`	System Description: E.T. 0.1. CADE Cezary Kaliszyk, Stephan Schulz, Josef Urban, Jirí Vyskocil
2014	J	`jnl`	Certified Connection Tableaux Proofs for HOL Light and TPTP. CoRR Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
2014	C	`conf`	Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description. CICM Cezary Kaliszyk, Josef Urban, Jirí Vyskocil, Herman Geuvers
2014	J	`jnl`	Developing Corpus-based Translation Methods between Informal and Formal Mathematics: Project Description. CoRR Cezary Kaliszyk, Josef Urban, Jirí Vyskocil, Herman Geuvers
2014	—	`ch.`	History of Interactive Theorem Proving. Computational Logic John Harrison, Josef Urban, Freek Wiedijk
2014	—	`conf`	Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems. ACL2 Sebastiaan J. C. Joosten, Cezary Kaliszyk, Josef Urban
2014	C	`ed.`	Intelligent Computer Mathematics - International Conference, CICM 2014, Coimbra, Portugal, July 7-11, 2014. Proceedings CICM Stephen M. Watt, James H. Davenport, Alan P. Sexton, Petr Sojka, Josef Urban
2014	—	`ed.`	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. CICM Workshops 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
2014	J	`jnl`	Learning-Assisted Automated Reasoning with Flyspeck. J. Autom. Reason. Cezary Kaliszyk, Josef Urban
2014	J	`jnl`	Learning-assisted Theorem Proving with Millions of Lemmas. CoRR Cezary Kaliszyk, Josef Urban
2014	—	`conf`	Machine Learner for Automated Reasoning 0.4 and 0.5. PAAR@IJCAR Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
2014	J	`jnl`	Machine Learner for Automated Reasoning 0.4 and 0.5. CoRR Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
2014	—	`conf`	Machine Learning of Coq Proof Guidance: First Experiments. SCSS Cezary Kaliszyk, Lionel Mamane, Josef Urban
2014	J	`jnl`	Machine Learning of Coq Proof Guidance: First Experiments. CoRR Cezary Kaliszyk, Lionel Mamane, Josef Urban
2014	J	`jnl`	Premise Selection for Mathematics by Corpus Analysis and Kernel Methods. J. Autom. Reason. Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze, Josef Urban
2014	—	`conf`	Wikis and Collaborative Systems for Large Formal Mathematics. SWCS (LNCS Volume) Cezary Kaliszyk, Josef Urban
2013	J	`jnl`	ATP and Presentation Service for Mizar Formalizations. J. Autom. Reason. Josef Urban, Piotr Rudnicki, Geoff Sutcliffe
2013	—	`conf`	Automated Reasoning Service for HOL Light. MKM/Calculemus/DML Cezary Kaliszyk, Josef Urban
2013	J	`jnl`	BliStr: The Blind Strategymaker CoRR Josef Urban
2013	B	`conf`	Communicating Formal Proofs: The Case of Flyspeck. ITP Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers
2013	A	`conf`	E-MaLeS 1.1. CADE Daniel Kühlwein, Stephan Schulz, Josef Urban
2013	J	`jnl`	Formal Mathematics on Display: A Wiki for Flyspeck CoRR Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers
2013	—	`conf`	Formal Mathematics on Display: A Wiki for Flyspeck. MKM/Calculemus/DML Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers
2013	J	`jnl`	HOL(y)Hammer: Online ATP Service for HOL Light. CoRR Cezary Kaliszyk, Josef Urban
2013	B	`conf`	Lemma Mining over HOL Light. LPAR Cezary Kaliszyk, Josef Urban
2013	J	`jnl`	Lemma Mining over HOL Light. CoRR Cezary Kaliszyk, Josef Urban
2013	J	`jnl`	MaLeS: A Framework for Automatic Tuning of Automated Theorem Provers. CoRR Daniel Kühlwein, Josef Urban
2013	B	`conf`	MaSh: Machine Learning for Sledgehammer. ITP Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, Josef Urban
2013	J	`jnl`	MizAR 40 for Mizar 40. CoRR Cezary Kaliszyk, Josef Urban
2013	A	`conf`	PRocH: Proof Reconstruction for HOL Light. CADE Cezary Kaliszyk, Josef Urban
2013	—	`conf`	Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution. PxTP@CADE Cezary Kaliszyk, Josef Urban
2013	J	`jnl`	The Mizar Mathematical Library in OMDoc: Translation and Applications. J. Autom. Reason. Mihnea Iancu, Michael Kohlhase, Florian Rabe, Josef Urban
2013	—	`conf`	Theorem Proving in Large Formal Mathematics as an Emerging AI Field. Automated Reasoning and Mathematics Josef Urban, Jirí Vyskocil
2013	—	`ed.`	Third International Workshop on Proof Exchange for Theorem Proving, PxTP 2013, Lake Placid, NY, USA, June 9-10, 2013 PxTP@CADE Jasmin Christian Blanchette, Josef Urban
2012	B	`conf`	Automated and Human Proofs in General Mathematics: An Initial Comparison. LPAR Jesse Alama, Daniel Kühlwein, Josef Urban
2012	—	`conf`	Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar. AISC/MKM/Calculemus Jesse Alama, Lionel Mamane, Josef Urban
2012	—	`conf`	Initial Experiments with External Provers and Premise Selection on HOL Light Corpora. PAAR@IJCAR Cezary Kaliszyk, Josef Urban
2012	—	`conf`	Learning from Multiple Proofs: First Experiments. PAAR@IJCAR Daniel Kühlwein, Josef Urban
2012	J	`jnl`	Learning-assisted Automated Reasoning with Flyspeck CoRR Cezary Kaliszyk, Josef Urban
2012	A	`conf`	Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics. IJCAR Daniel Kühlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban, Tom Heskes
2012	J	`jnl`	Parallelizing Mizar CoRR Josef Urban
2012	—	`conf`	Point-and-Write - Documenting Formal Mathematics by Reference. AISC/MKM/Calculemus Carst Tankink, Christoph Lange, Josef Urban
2012	J	`jnl`	Point-and-write --- Documenting Formal Mathematics by Reference CoRR Carst Tankink, Christoph Lange, Josef Urban
2012	J	`jnl`	Theorem Proving in Large Formal Mathematics as an Emerging AI Field CoRR Josef Urban, Jirí Vyskocil
2011	J	`jnl`	ATP and Presentation Service for Mizar Formalizations CoRR Josef Urban, Piotr Rudnicki, Geoff Sutcliffe
2011	—	`conf`	An Overview of Methods for Large-Theory Automated Theorem Proving. ATE Josef Urban
2011	—	`conf`	Content-based encoding of mathematical and code libraries. MathWikis@ITP Josef Urban
2011	J	`jnl`	Dependencies in Formal Mathematics CoRR Jesse Alama, Lionel Mamane, Josef Urban
2011	—	`conf`	Escape to ATP for Mizar. PxTP Piotr Rudnicki, Josef Urban
2011	—	`ed.`	Intelligent Computer Mathematics - 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011. Proceedings Calculemus/MKM James H. Davenport, William M. Farmer, Josef Urban, Florian Rabe
2011	J	`jnl`	Large Formal Wikis: Issues and Solutions CoRR Jesse Alama, Kasper Brink, Lionel Mamane, Josef Urban
2011	—	`conf`	Large Formal Wikis: Issues and Solutions. Calculemus/MKM Jesse Alama, Kasper Brink, Lionel Mamane, Josef Urban
2011	—	`conf`	Learning2Reason. Calculemus/MKM Daniel Kühlwein, Josef Urban, Evgeni Tsivtsivadze, Herman Geuvers, Tom Heskes
2011	J	`jnl`	Licensing the Mizar Mathematical Library CoRR Jesse Alama, Michael Kohlhase, Adam Naumowicz, Piotr Rudnicki, Josef Urban, Lionel Mamane
2011	—	`conf`	Licensing the Mizar Mathematical Library. Calculemus/MKM Jesse Alama, Michael Kohlhase, Lionel Mamane, Adam Naumowicz, Piotr Rudnicki, Josef Urban
2011	B	`conf`	MaLeCoP Machine Learning Connection Prover. TABLEAUX Josef Urban, Jirí Vyskocil, Petr Stepánek
2011	—	`conf`	Multi-output Ranking for Automated Reasoning. KDIR Daniel Kühlwein, Josef Urban, Evgeni Tsivtsivadze, Herman Geuvers, Tom Heskes
2011	J	`jnl`	Premise Selection for Mathematics by Corpus Analysis and Kernel Methods CoRR Jesse Alama, Daniel Kühlwein, Evgeni Tsivtsivadze, Josef Urban, Tom Heskes
2011	—	`ed.`	Proceedings of the ITP 2011 Workshop on Mathematical Wikis, Nijmegen, The Netherlands, August 27th, 2011 MathWikis@ITP Christoph Lange, Josef Urban
2011	A	`conf`	Semantic Graph Kernels for Automated Reasoning. SDM Evgeni Tsivtsivadze, Josef Urban, Herman Geuvers, Tom Heskes
2010	J	`jnl`	A Wiki for Mizar: Motivation, Considerations, and Initial Prototype CoRR Josef Urban, Jesse Alama, Piotr Rudnicki, Herman Geuvers
2010	—	`conf`	A Wiki for Mizar: Motivation, Considerations, and Initial Prototype. AISC/MKM/Calculemus Josef Urban, Jesse Alama, Piotr Rudnicki, Herman Geuvers
2010	—	`conf`	Automated Proof Compression by Invention of New Definitions. LPAR (Dakar) Jirí Vyskocil, David Stanovský, Josef Urban
2010	J	`jnl`	Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar CoRR Josef Urban, Geoff Sutcliffe
2010	—	`conf`	Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar. AISC/MKM/Calculemus Josef Urban, Geoff Sutcliffe
2010	—	`conf`	Evaluation of Automated Theorem Proving on the Mizar Mathematical Library. ICMS Josef Urban, Krystof Hoder, Andrei Voronkov
2008	J	`jnl`	ATP-based Cross-Verification of Mizar Proofs: Method, Systems, and First Experiments. Math. Comput. Sci. Josef Urban, Geoff Sutcliffe
2008	—	`conf`	Automated Reasoning for Mizar: Artificial Intelligence through Knowledge Exchange. LPAR Workshops Josef Urban
2008	A	`conf`	MaLARea SG1- Machine Learner for Automated Reasoning with Semantic Guidance. IJCAR Josef Urban, Geoff Sutcliffe, Petr Pudlák, Jirí Vyskocil
2007	B	`conf`	ATP Cross-Verification of the Mizar MPTP Challenge Problems. LPAR Josef Urban, Geoff Sutcliffe
2007	—	`conf`	MaLARea: a Metasystem for Automated Reasoning in Large Theories. ESARLT Josef Urban
2007	—	`ed.`	Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, Bremen, Germany, 17th July 2007 ESARLT Geoff Sutcliffe, Josef Urban, Stephan Schulz
2006	J	`jnl`	MPTP 0.2: Design, Implementation, and Initial Experiments. J. Autom. Reason. Josef Urban
2006	J	`jnl`	MizarMode - an integrated proof assistance tool for the Mizar way of formalizing mathematics. J. Appl. Log. Josef Urban
2006	J	`jnl`	Momm - Fast Interreduction and Retrieval in Large Libraries of Formalized Mathematics. Int. J. Artif. Intell. Tools Josef Urban
2006	—	`conf`	Presenting and Explaining Mizar. UITP@FLoC Josef Urban, Grzegorz Bancerek
2005	—	`conf`	XML-izing Mizar: Making Semantic Processing and Presentation of MML Easy. MKM Josef Urban
2004	—	`conf`	Integrated Semantic Browsing of the Mizar Mathematical Library for Authoring Mizar Articles. MKM Grzegorz Bancerek, Josef Urban
2004	J	`jnl`	MPTP - Motivation, Implementation, First Experiments. J. Autom. Reason. Josef Urban
2003	—	`conf`	MPTP 0.1: System Description. FTP Josef Urban
2003	—	`conf`	Translating Mizar for First Order Theorem Provers. MKM Josef Urban
2001	J	`jnl`	BRAIN - an architecture for a broadband radio access network of the next generation. Wirel. Commun. Mob. Comput. Josef Urban, Dave Wisely, Edgar Bolinth, Georg Neureiter, Mika Liljeberg, Tomás Robles Valladares
2000	B	`conf`	Broadband Radio Access for IP-based networks (BRAIN)-a key enabler for mobile Internet access. PIMRC Dave Wisely, Werner Mohr, Josef Urban