Jan Jakubuv

Publication Activity (10 Years)

Years Active: 2010-2024
Publications (10 Years): 46

Top Topics

Multiagent Planning

Automated Reasoning

Theorem Proving

Top Venues

Trans. Comput. Collect. Intell.

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)
Kristina Aleksandrova, Jan Jakubuv, Cezary Kaliszyk
Prover9 Unleashed: Automated Configuration for Enhanced Proof Discovery. 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)
Jan Jakubuv, Cezary Kaliszyk
VizAR: Visualization of Automated Reasoning Proofs (System Description). CICM (2023)
Jan Jakubuv, Mikolás Janota, Bartosz Piotrowski, Jelle Piepenbrock, Andrew Reynolds
Selecting Quantifiers for Instantiation in SMT. SMT (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)
Jan Hula, Jan Jakubuv, Mikolás Janota, Lukás Kubej
Targeted Configuration of an SMT Solver. CICM (2022)
Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban
Learning Theorem Proving Components. TABLEAUX (2021)
Jan Jakubuv, Mikolás Janota, Andrew Reynolds
Characteristic Subsets of SMT-LIB Benchmarks. SMT (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)
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)
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)
Jan Jakubuv, Cezary Kaliszyk
Relaxed Weighted Path Order in Theorem Proving. Math. Comput. Sci. 14 (3) (2020)
Josef Urban, Jan Jakubuv
First Neural Conjecturing Datasets and Experiments. CoRR (2020)
Zarathustra Amadeus Goertzel, Jan Jakubuv, Josef Urban
ENIGMAWatch: ProofWatch Meets ENIGMA. TABLEAUX (2019)
Karel Chvalovský, Jan Jakubuv, Martin Suda, Josef Urban
ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E. 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)
Jan Jakubuv, Cezary Kaliszyk
Towards a Unified Ordering for Superposition-Based Automated Reasoning. ICMS (2018)
Zarathustra Amadeus Goertzel, Jan Jakubuv, Stephan Schulz, Josef Urban
ProofWatch: Watchlist Guidance for Large Theories in E. CoRR (2018)
Zarathustra Amadeus Goertzel, Jan Jakubuv, Stephan Schulz, Josef Urban
ProofWatch: Watchlist Guidance for Large Theories in E. ITP (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 Tozicka, Jan Jakubuv, Antonín Komenda
Recursive Reductions of Action Dependencies for Coordination-Based Multiagent Planning. Trans. Comput. Collect. Intell. 28 (2018)
Jan Jakubuv, Josef Urban
Enhancing ENIGMA Given Clause Guidance. CICM (2018)
Jan Jakubuv, Josef Urban
ENIGMA: Efficient Learning-Based Inference Guiding Machine. CICM (2017)
Jan Jakubuv, Josef Urban
BliStrTune: hierarchical invention of theorem proving strategies. CPP (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)
Jan Tozicka, Jan Jakubuv, Antonín Komenda
Recursive Reductions of Internal Dependencies in Multiagent Planning. ICAART (2) (2016)
Jan Jakubuv, Josef Urban
Extending E Prover with Similarity Based Clause Selection Strategies. CoRR (2016)
Jan Jakubuv, Josef Urban
Extending E Prover with Similarity Based Clause Selection Strategies. CICM (2016)
Jan Tozicka, Jan Jakubuv, Martin Svatos, Antonín Komenda
Recursive Polynomial Reductions for Classical Planning. ICAPS (2016)
Jan Jakubuv, Josef Urban
BliStrTune: Hierarchical Invention of Theorem Proving Strategies. CoRR (2016)
Jan Tozicka, Jan Jakubuv, Antonín Komenda, Michal Pechoucek
Privacy-concerned multiagent planning. Knowl. Inf. Syst. 48 (3) (2016)
Jan Tozicka, Jan Jakubuv, Karel Durkota, Antonín Komenda
Extensibility Based Multiagent Planner with Plan Diversity Metrics. Trans. Comput. Collect. Intell. 20 (2015)
Jan Jakubuv, Jan Tozicka, Antonín Komenda
Multiagent Planning by Plan Set Intersection and Plan Verification. ICAART (2) (2015)
Jan Tozicka, Jan Jakubuv, Antonín Komenda
From Public Plans to Global Solutions in Multiagent Planning. EUMAS/AT (2015)
Jan Jakubuv, Jan Tozicka, Antonín Komenda
Using Process Calculi for Plan Verification in Multiagent Planning. ICAART (Revised Selected Papers) (2015)
Jan Tozicka, Jan Jakubuv, Karel Durkota, Antonín Komenda, Michal Pechoucek
Multiagent Planning Supported by Plan Diversity Metrics and Landmark Actions. ICAART (1) (2014)
Jan Tozicka, Jan Jakubuv, Antonín Komenda
Generating Multi-Agent Plans by Distributed Intersection of Finite State Machines. ECAI (2014)
Jan Jakubuv, J. B. Wells
Expressiveness of Generic Process Shape Types. TGC (2010)
Jan Jakubuv, J. B. Wells
Expressiveness of Generic Process Shape Types CoRR (2010)