Josef Urban

Orcid: 0000-0002-1384-1613

According to our database1, Josef Urban authored at least 155 papers between 2000 and 2025.

Collaborative distances:

Timeline

2000
2005
2010
2015
2020
2025
0
5
10
15
20
1
1
1
3
3
3
3
5
7
6
2
2
1
1
1
3
1
1
4
7
3
6
9
4
7
9
6
12
5
9
6
9
4
2
2
1
1
1
2
1

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

On csauthors.net:

Bibliography

2025
Invariant neural architecture for learning term synthesis in instantiation proving.
J. Symb. Comput., 2025

2024
Solving Hard Mizar Problems with Instantiation and Strategy Invention.
Proceedings of the Intelligent Computer Mathematics - 17th International Conference, 2024

First Experiments with Neural cvc5.
Proceedings of the LPAR 2024: Proceedings of 25th Conference on Logic for Programming, 2024

Machine Learning for Quantifier Selection in cvc5.
Proceedings of the ECAI 2024 - 27th European Conference on Artificial Intelligence, 19-24 October 2024, Santiago de Compostela, Spain, 2024

Learning Guided Automated Reasoning: A Brief Survey.
Proceedings of the Logics and Type Systems in Theory and Practice, 2024

2023
Alien coding.
Int. J. Approx. Reason., November, 2023

A Mathematical Benchmark for Inductive Theorem Provers.
Proceedings of the LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, 2023

Guiding an Instantiation Prover with Graph Neural Networks.
Proceedings of the LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, 2023

MizAR 60 for Mizar 50.
Proceedings of the 14th International Conference on Interactive Theorem Proving, 2023

Automated Theorem Proving for Metamath.
Proceedings of the 14th International Conference on Interactive Theorem Proving, 2023

Learning Proof Transformations and Its Applications in Interactive Theorem Proving.
Proceedings of the Frontiers of Combining Systems - 14th International Symposium, 2023

Translating SUMO-K to Higher-Order Set Theory.
Proceedings of the Frontiers of Combining Systems - 14th International Symposium, 2023

Learning Program Synthesis for Integer Sequences from Scratch.
Proceedings of the Thirty-Seventh AAAI Conference on Artificial Intelligence, 2023

2022
Machine Learning Meets The Herbrand Universe.
CoRR, 2022

PREVIEW VERSION: Six Insights into 6G: Orientation and Input for Developing Your Strategic 6G Research Plan.
CoRR, 2022

Six Questions about 6G.
CoRR, 2022

The Isabelle ENIGMA.
Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

Proofgold: Blockchain for Formal Methods.
Proceedings of the 4th International Workshop on Formal Methods for Blockchains, 2022

Guiding an Automated Theorem Prover with Neural Rewriting.
Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

2021
TacticToe: Learning to Prove with Tactics.
J. Autom. Reason., 2021

Machine Learning Guidance for Connection Tableaux.
J. Autom. Reason., 2021

Learning Equational Theorem Proving.
CoRR, 2021

The Role of Entropy in Guiding a Connection Prover.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2021

Towards Finding Longer Proofs.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2021

Learning Theorem Proving Components.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2021

Online Machine Learning Techniques for Coq: A Comparison.
Proceedings of the Intelligent Computer Mathematics - 14th International Conference, 2021

Learning to Solve Geometric Construction Problems from Images.
Proceedings of the Intelligent Computer Mathematics - 14th International Conference, 2021

Fast and Slow Enigmas and Parental Guidance.
Proceedings of the Frontiers of Combining Systems - 13th International Symposium, 2021

2020
Foreword.
Math. Comput. Sci., 2020

The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq.
CoRR, 2020

Prolog Technology Reinforcement Learning Prover.
CoRR, 2020

First Neural Conjecturing Datasets and Experiments.
Proceedings of the Intelligent Computer Mathematics - 13th International Conference, 2020

Guiding Inferences in Connection Tableau by Recurrent Neural Networks.
Proceedings of the Intelligent Computer Mathematics - 13th International Conference, 2020

The Tactician - A Seamless, Interactive Tactic Learner and Prover for Coq.
Proceedings of the Intelligent Computer Mathematics - 13th International Conference, 2020

Stateful Premise Selection by Recurrent Neural Networks.
Proceedings of the LPAR 2020: 23rd International Conference on Logic for Programming, 2020

Tactic Learning and Proving for the Coq Proof Assistant.
Proceedings of the LPAR 2020: 23rd International Conference on Logic for Programming, 2020

Property Invariant Embedding for Automated Reasoning.
Proceedings of the ECAI 2020 - 24th European Conference on Artificial Intelligence, 29 August-8 September 2020, Santiago de Compostela, Spain, August 29 - September 8, 2020, 2020

Exploration of neural machine translation in autoformalization of mathematics in Mizar.
Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020

Prolog Technology Reinforcement Learning Prover - (System Description).
Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description).
Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019
Can Neural Networks Learn Symbolic Rewriting?
CoRR, 2019

Guiding Theorem Proving by Recurrent Neural Networks.
CoRR, 2019

Hammering Mizar by Learning Clause Guidance.
CoRR, 2019

ENIGMAWatch: ProofWatch Meets ENIGMA.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2019

Hammering Mizar by Learning Clause Guidance (Short Paper).
Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E.
Proceedings of the Automated Deduction - CADE 27, 2019

GRUNGE: A Grand Unified ATP Challenge.
Proceedings of the Automated Deduction - CADE 27, 2019

2018
Machine Learning Guidance and Proof Certification for Connection Tableaux.
CoRR, 2018

Learning to Prove with Tactics.
CoRR, 2018

Learning to Reason with HOL4 tactics.
CoRR, 2018

Hierarchical invention of theorem proving strategies.
AI Commun., 2018

Foreword to the Special Issue on Automated Reasoning.
AI Commun., 2018

Reinforcement Learning of Theorem Proving.
Proceedings of the Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, 2018

First Experiments with Neural Translation of Informal to Formal Mathematics.
Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2018

Enhancing ENIGMA Given Clause Guidance.
Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2018

System Description: XSL-Based Translator of Mizar to LaTeX.
Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2018

ProofWatch Meets ENIGMA: First Experiments.
Proceedings of the LPAR-22 Workshop and Short Paper Proceedings, 2018

ProofWatch: Watchlist Guidance for Large Theories in E.
Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback.
Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

2017
System Description: Statistical Parsing of Informalized Mizar Formulas.
Proceedings of the 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2017

ENIGMA: Efficient Learning-Based Inference Guiding Machine.
Proceedings of the Intelligent Computer Mathematics - 10th International Conference, 2017

TacticToe: Learning to Reason with HOL4 Tactics.
Proceedings of the LPAR-21, 2017

Automating Formalization by Statistical and Semantic Parsing of Mathematics.
Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017

Automated Invention of Strategies and Term Orderings for Vampire.
Proceedings of the GCAI 2017, 2017

BliStrTune: hierarchical invention of theorem proving strategies.
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

AI at CADE/IJCAR.
Proceedings of the ARCADE 2017, 2017

Monte Carlo Tableau Proof Search.
Proceedings of the Automated Deduction - CADE 26, 2017

Detecting Inconsistencies in Large First-Order Knowledge Bases.
Proceedings of the Automated Deduction - CADE 26, 2017

2016
Preface: Twenty Years of the QED Manifesto.
J. Formaliz. Reason., 2016

Hammering towards QED.
J. Formaliz. Reason., 2016

A Learning-Based Fact Selector for Isabelle/HOL.
J. Autom. Reason., 2016

Semantic Parsing of Mathematics by Context-based Learning from Aligned Corpora and Theorem Proving.
CoRR, 2016

Monte Carlo Connection Prover.
CoRR, 2016

DeepMath - Deep Sequence Models for Premise Selection.
CoRR, 2016

The CADE-25 Automated Theorem Proving system competition - CASC-25.
AI Commun., 2016

DeepMath - Deep Sequence Models for Premise Selection.
Proceedings of the Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Processing Systems 2016, 2016

Extending E Prover with Similarity Based Clause Selection Strategies.
Proceedings of the Intelligent Computer Mathematics - 9th International Conference, 2016

Extracting Higher-Order Goals from the Mizar Mathematical Library.
Proceedings of the Intelligent Computer Mathematics - 9th International Conference, 2016

Learning Intelligent Theorem Proving from Large Formal Corpora.
Proceedings of the International Symposium on Artificial Intelligence and Mathematics, 2016

Towards a mizar environment for isabelle: foundations and language.
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016

Initial Experiments with Statistical Conjecturing over Large Formal Corpora.
Proceedings of the Joint Proceedings of the FM4M, 2016

2015
HOL(y)Hammer: Online ATP Service for HOL Light.
Math. Comput. Sci., 2015

Learning-assisted theorem proving with millions of lemmas.
J. Symb. Comput., 2015

MaLeS: A Framework for Automatic Tuning of Automated Theorem Provers.
J. Autom. Reason., 2015

MizAR 40 for Mizar 40.
J. Autom. Reason., 2015

Erratum to : Learning-Assisted Automated Reasoning with Flyspeck.
J. Autom. Reason., 2015

A formal proof of the Kepler conjecture.
CoRR, 2015

Formalizing Physics: Automation, Presentation and Foundation Issues.
Proceedings of the Intelligent Computer Mathematics - International Conference, 2015

Auto-hyperlinking the Stacks Project.
Proceedings of the CICM 2015, 2015

Mizar: State-of-the-art and Beyond.
Proceedings of the Intelligent Computer Mathematics - International Conference, 2015

Experiments with State-of-the-art Automated Provers on Problems in Tarskian Geometry.
Proceedings of the IWIL@LPAR 2015, 2015

Improving Statistical Linguistic Algorithms for Parsing Mathematics.
Proceedings of the IWIL@LPAR 2015, 2015

FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

Learning to Parse on Aligned Corpora (Rough Diamond).
Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

Efficient Semantic Features for Automated Reasoning over Large Theories.
Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, 2015

BliStr: The Blind Strategymaker.
Proceedings of the Global Conference on Artificial Intelligence, 2015

Lemmatization for Stronger Reasoning in Large Theories.
Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015

Certified Connection Tableaux Proofs for HOL Light and TPTP.
Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015

System Description: E.T. 0.1.
Proceedings of the Automated Deduction - CADE-25, 2015

2014
History of Interactive Theorem Proving.
Proceedings of the Computational Logic, 2014

Learning-Assisted Automated Reasoning with Flyspeck.
J. Autom. Reason., 2014

Premise Selection for Mathematics by Corpus Analysis and Kernel Methods.
J. Autom. Reason., 2014

Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems.
Proceedings of the Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications, 2014

Machine Learning of Coq Proof Guidance: First Experiments.
Proceedings of the 6th International Symposium on Symbolic Computation in Software Science, 2014

Wikis and Collaborative Systems for Large Formal Mathematics.
Proceedings of the Semantic Web Collaborative Spaces, 2014

Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description.
Proceedings of the Intelligent Computer Mathematics - International Conference, 2014

Machine Learner for Automated Reasoning 0.4 and 0.5.
Proceedings of the 4th Workshop on Practical Aspects of Automated Reasoning, 2014

2013
ATP and Presentation Service for Mizar Formalizations.
J. Autom. Reason., 2013

The Mizar Mathematical Library in OMDoc: Translation and Applications.
J. Autom. Reason., 2013

Formal Mathematics on Display: A Wiki for Flyspeck.
Proceedings of the Intelligent Computer Mathematics, 2013

Automated Reasoning Service for HOL Light.
Proceedings of the Intelligent Computer Mathematics, 2013

Lemma Mining over HOL Light.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2013

Communicating Formal Proofs: The Case of Flyspeck.
Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

MaSh: Machine Learning for Sledgehammer.
Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

E-MaLeS 1.1.
Proceedings of the Automated Deduction - CADE-24, 2013

Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution.
Proceedings of the Third International Workshop on Proof Exchange for Theorem Proving, 2013

PRocH: Proof Reconstruction for HOL Light.
Proceedings of the Automated Deduction - CADE-24, 2013

Theorem Proving in Large Formal Mathematics as an Emerging AI Field.
Proceedings of the Automated Reasoning and Mathematics, 2013

2012
Parallelizing Mizar
CoRR, 2012

Automated and Human Proofs in General Mathematics: An Initial Comparison.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

Learning from Multiple Proofs: First Experiments.
Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning, 2012

Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics.
Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

Initial Experiments with External Provers and Premise Selection on HOL Light Corpora.
Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning, 2012

Point-and-Write - Documenting Formal Mathematics by Reference.
Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2012

Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar.
Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2012

2011
Dependencies in Formal Mathematics
CoRR, 2011

MaLeCoP Machine Learning Connection Prover.
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2011

Semantic Graph Kernels for Automated Reasoning.
Proceedings of the Eleventh SIAM International Conference on Data Mining, 2011

Escape to ATP for Mizar.
Proceedings of the PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, 2011

Learning2Reason.
Proceedings of the Intelligent Computer Mathematics - 18th Symposium, 2011

Licensing the Mizar Mathematical Library.
Proceedings of the Intelligent Computer Mathematics - 18th Symposium, 2011

Large Formal Wikis: Issues and Solutions.
Proceedings of the Intelligent Computer Mathematics - 18th Symposium, 2011

Content-based encoding of mathematical and code libraries.
Proceedings of the ITP 2011 Workshop on Mathematical Wikis, 2011

Multi-output Ranking for Automated Reasoning.
Proceedings of the KDIR 2011, 2011

An Overview of Methods for Large-Theory Automated Theorem Proving.
Proceedings of the First Workshop on Automated Theory Engineering, 2011

2010
Automated Proof Compression by Invention of New Definitions.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

Evaluation of Automated Theorem Proving on the Mizar Mathematical Library.
Proceedings of the Mathematical Software, 2010

Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar.
Proceedings of the Intelligent Computer Mathematics, 10th International Conference, 2010

A Wiki for Mizar: Motivation, Considerations, and Initial Prototype.
Proceedings of the Intelligent Computer Mathematics, 10th International Conference, 2010

2008
ATP-based Cross-Verification of Mizar Proofs: Method, Systems, and First Experiments.
Math. Comput. Sci., 2008

Automated Reasoning for Mizar: Artificial Intelligence through Knowledge Exchange.
Proceedings of the LPAR 2008 Workshops, 2008

MaLARea SG1- Machine Learner for Automated Reasoning with Semantic Guidance.
Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

2007
ATP Cross-Verification of the Mizar MPTP Challenge Problems.
Proceedings of the Logic for Programming, 2007

MaLARea: a Metasystem for Automated Reasoning in Large Theories.
Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, 2007

2006
MPTP 0.2: Design, Implementation, and Initial Experiments.
J. Autom. Reason., 2006

MizarMode - an integrated proof assistance tool for the Mizar way of formalizing mathematics.
J. Appl. Log., 2006

Momm - Fast Interreduction and Retrieval in Large Libraries of Formalized Mathematics.
Int. J. Artif. Intell. Tools, 2006

Presenting and Explaining Mizar.
Proceedings of the 7th Workshop on User Interfaces for Theorem Provers, 2006

2005
XML-izing Mizar: Making Semantic Processing and Presentation of MML Easy.
Proceedings of the Mathematical Knowledge Management, 4th International Conference, 2005

2004
MPTP - Motivation, Implementation, First Experiments.
J. Autom. Reason., 2004

Integrated Semantic Browsing of the Mizar Mathematical Library for Authoring Mizar Articles.
Proceedings of the Mathematical Knowledge Management, Third International Conference, 2004

2003
MPTP 0.1: System Description.
Proceedings of the 4th International Workshop on First-Order Theorem Proving, 2003

Translating Mizar for First Order Theorem Provers.
Proceedings of the Mathematical Knowledge Management, Second International Conference, 2003

2001
BRAIN - an architecture for a broadband radio access network of the next generation.
Wirel. Commun. Mob. Comput., 2001

2000
Broadband Radio Access for IP-based networks (BRAIN)-a key enabler for mobile Internet access.
Proceedings of the 11th IEEE International Symposium on Personal, 2000


  Loading...