BibTeX records: Jan Jakubuv

download as .bib file

@inproceedings{DBLP:conf/itp/JakubuvCGKOP00U23,
  author       = {Jan Jakubuv and
                  Karel Chvalovsk{\'{y}} and
                  Zarathustra Amadeus Goertzel and
                  Cezary Kaliszyk and
                  Mirek Ols{\'{a}}k and
                  Bartosz Piotrowski and
                  Stephan Schulz and
                  Martin Suda and
                  Josef Urban},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {MizAR 60 for Mizar 50},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {19:1--19:22},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.19},
  doi          = {10.4230/LIPICS.ITP.2023.19},
  timestamp    = {Wed, 26 Jul 2023 16:07:09 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/JakubuvCGKOP00U23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/mkm/JakubuvK23,
  author       = {Jan Jakubuv and
                  Cezary Kaliszyk},
  editor       = {Catherine Dubois and
                  Manfred Kerber},
  title        = {VizAR: Visualization of Automated Reasoning Proofs (System Description)},
  booktitle    = {Intelligent Computer Mathematics - 16th International Conference,
                  {CICM} 2023, Cambridge, UK, September 5-8, 2023, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {14101},
  pages        = {303--308},
  publisher    = {Springer},
  year         = {2023},
  url          = {https://doi.org/10.1007/978-3-031-42753-4\_22},
  doi          = {10.1007/978-3-031-42753-4\_22},
  timestamp    = {Thu, 14 Sep 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/mkm/JakubuvK23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/smt/JakubuvJPP023,
  author       = {Jan Jakubuv and
                  Mikol{\'{a}}s Janota and
                  Bartosz Piotrowski and
                  Jelle Piepenbrock and
                  Andrew Reynolds},
  editor       = {St{\'{e}}phane Graham{-}Lengrand and
                  Mathias Preiner},
  title        = {Selecting Quantifiers for Instantiation in {SMT}},
  booktitle    = {Proceedings of the 21st International Workshop on Satisfiability Modulo
                  Theories {(SMT} 2023) co-located with the 29th International Conference
                  on Automated Deduction {(CADE} 2023), Rome, Italy, July, 5-6, 2023},
  series       = {{CEUR} Workshop Proceedings},
  volume       = {3429},
  pages        = {71--77},
  publisher    = {CEUR-WS.org},
  year         = {2023},
  url          = {https://ceur-ws.org/Vol-3429/short10.pdf},
  timestamp    = {Wed, 05 Jul 2023 16:52:15 +0200},
  biburl       = {https://dblp.org/rec/conf/smt/JakubuvJPP023.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2303-06686,
  author       = {Jan Jakubuv and
                  Karel Chvalovsk{\'{y}} and
                  Zarathustra Amadeus Goertzel and
                  Cezary Kaliszyk and
                  Mirek Ols{\'{a}}k and
                  Bartosz Piotrowski and
                  Stephan Schulz and
                  Martin Suda and
                  Josef Urban},
  title        = {MizAR 60 for Mizar 50},
  journal      = {CoRR},
  volume       = {abs/2303.06686},
  year         = {2023},
  url          = {https://doi.org/10.48550/arXiv.2303.06686},
  doi          = {10.48550/ARXIV.2303.06686},
  eprinttype    = {arXiv},
  eprint       = {2303.06686},
  timestamp    = {Thu, 16 Mar 2023 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/corr/abs-2303-06686.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/GoertzelJKOPU22,
  author       = {Zarathustra Amadeus Goertzel and
                  Jan Jakubuv and
                  Cezary Kaliszyk and
                  Miroslav Ols{\'{a}}k and
                  Jelle Piepenbrock and
                  Josef Urban},
  editor       = {June Andronick and
                  Leonardo de Moura},
  title        = {The Isabelle {ENIGMA}},
  booktitle    = {13th International Conference on Interactive Theorem Proving, {ITP}
                  2022, August 7-10, 2022, Haifa, Israel},
  series       = {LIPIcs},
  volume       = {237},
  pages        = {16:1--16:21},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2022},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2022.16},
  doi          = {10.4230/LIPICS.ITP.2022.16},
  timestamp    = {Tue, 21 Mar 2023 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/conf/itp/GoertzelJKOPU22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/mkm/HulaJJK22,
  author       = {Jan Hula and
                  Jan Jakubuv and
                  Mikol{\'{a}}s Janota and
                  Luk{\'{a}}s Kubej},
  editor       = {Kevin Buzzard and
                  Temur Kutsia},
  title        = {Targeted Configuration of an {SMT} Solver},
  booktitle    = {Intelligent Computer Mathematics - 15th International Conference,
                  {CICM} 2022, Tbilisi, Georgia, September 19-23, 2022, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {13467},
  pages        = {256--271},
  publisher    = {Springer},
  year         = {2022},
  url          = {https://doi.org/10.1007/978-3-031-16681-5\_18},
  doi          = {10.1007/978-3-031-16681-5\_18},
  timestamp    = {Mon, 19 Sep 2022 18:41:39 +0200},
  biburl       = {https://dblp.org/rec/conf/mkm/HulaJJK22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2205-01981,
  author       = {Zarathustra Amadeus Goertzel and
                  Jan Jakubuv and
                  Cezary Kaliszyk and
                  Miroslav Ols{\'{a}}k and
                  Jelle Piepenbrock and
                  Josef Urban},
  title        = {The Isabelle {ENIGMA}},
  journal      = {CoRR},
  volume       = {abs/2205.01981},
  year         = {2022},
  url          = {https://doi.org/10.48550/arXiv.2205.01981},
  doi          = {10.48550/ARXIV.2205.01981},
  eprinttype    = {arXiv},
  eprint       = {2205.01981},
  timestamp    = {Thu, 05 May 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/abs-2205-01981.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/frocos/GoertzelCJOU21,
  author       = {Zarathustra Amadeus Goertzel and
                  Karel Chvalovsk{\'{y}} and
                  Jan Jakubuv and
                  Miroslav Ols{\'{a}}k and
                  Josef Urban},
  editor       = {Boris Konev and
                  Giles Reger},
  title        = {Fast and Slow Enigmas and Parental Guidance},
  booktitle    = {Frontiers of Combining Systems - 13th International Symposium, FroCoS
                  2021, Birmingham, UK, September 8-10, 2021, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {12941},
  pages        = {173--191},
  publisher    = {Springer},
  year         = {2021},
  url          = {https://doi.org/10.1007/978-3-030-86205-3\_10},
  doi          = {10.1007/978-3-030-86205-3\_10},
  timestamp    = {Mon, 03 Jan 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/conf/frocos/GoertzelCJOU21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/smt/JakubuvJR21,
  author       = {Jan Jakubuv and
                  Mikol{\'{a}}s Janota and
                  Andrew Reynolds},
  editor       = {Alexander Nadel and
                  Aina Niemetz},
  title        = {Characteristic Subsets of {SMT-LIB} Benchmarks},
  booktitle    = {Proceedings of the 19th International Workshop on Satisfiability Modulo
                  Theories co-located with 33rd International Conference on Computer
                  Aided Verification(CAV 2021), Online (initially located in Los Angeles,
                  USA), July 18-19, 2021},
  series       = {{CEUR} Workshop Proceedings},
  volume       = {2908},
  pages        = {53--63},
  publisher    = {CEUR-WS.org},
  year         = {2021},
  url          = {https://ceur-ws.org/Vol-2908/paper7.pdf},
  timestamp    = {Fri, 10 Mar 2023 16:22:48 +0100},
  biburl       = {https://dblp.org/rec/conf/smt/JakubuvJR21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tableaux/ChvalovskyJOU21,
  author       = {Karel Chvalovsk{\'{y}} and
                  Jan Jakubuv and
                  Miroslav Ols{\'{a}}k and
                  Josef Urban},
  editor       = {Anupam Das and
                  Sara Negri},
  title        = {Learning Theorem Proving Components},
  booktitle    = {Automated Reasoning with Analytic Tableaux and Related Methods - 30th
                  International Conference, {TABLEAUX} 2021, Birmingham, UK, September
                  6-9, 2021, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {12842},
  pages        = {266--278},
  publisher    = {Springer},
  year         = {2021},
  url          = {https://doi.org/10.1007/978-3-030-86059-2\_16},
  doi          = {10.1007/978-3-030-86059-2\_16},
  timestamp    = {Thu, 16 Sep 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/tableaux/ChvalovskyJOU21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2107-06750,
  author       = {Zarathustra Amadeus Goertzel and
                  Karel Chvalovsk{\'{y}} and
                  Jan Jakubuv and
                  Miroslav Ols{\'{a}}k and
                  Josef Urban},
  title        = {Fast and Slow Enigmas and Parental Guidance},
  journal      = {CoRR},
  volume       = {abs/2107.06750},
  year         = {2021},
  url          = {https://arxiv.org/abs/2107.06750},
  eprinttype    = {arXiv},
  eprint       = {2107.06750},
  timestamp    = {Sat, 28 Aug 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/abs-2107-06750.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2107-10034,
  author       = {Karel Chvalovsk{\'{y}} and
                  Jan Jakubuv and
                  Miroslav Ols{\'{a}}k and
                  Josef Urban},
  title        = {Learning Theorem Proving Components},
  journal      = {CoRR},
  volume       = {abs/2107.10034},
  year         = {2021},
  url          = {https://arxiv.org/abs/2107.10034},
  eprinttype    = {arXiv},
  eprint       = {2107.10034},
  timestamp    = {Thu, 29 Jul 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/abs-2107-10034.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/mics/JakubuvK20,
  author       = {Jan Jakubuv and
                  Cezary Kaliszyk},
  title        = {Relaxed Weighted Path Order in Theorem Proving},
  journal      = {Math. Comput. Sci.},
  volume       = {14},
  number       = {3},
  pages        = {657--670},
  year         = {2020},
  url          = {https://doi.org/10.1007/s11786-020-00474-0},
  doi          = {10.1007/S11786-020-00474-0},
  timestamp    = {Wed, 16 Mar 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/mics/JakubuvK20.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/JakubuvCOP0U20,
  author       = {Jan Jakubuv and
                  Karel Chvalovsk{\'{y}} and
                  Miroslav Ols{\'{a}}k and
                  Bartosz Piotrowski and
                  Martin Suda and
                  Josef Urban},
  editor       = {Nicolas Peltier and
                  Viorica Sofronie{-}Stokkermans},
  title        = {{ENIGMA} Anonymous: Symbol-Independent Inference Guiding Machine (System
                  Description)},
  booktitle    = {Automated Reasoning - 10th International Joint Conference, {IJCAR}
                  2020, Paris, France, July 1-4, 2020, Proceedings, Part {II}},
  series       = {Lecture Notes in Computer Science},
  volume       = {12167},
  pages        = {448--463},
  publisher    = {Springer},
  year         = {2020},
  url          = {https://doi.org/10.1007/978-3-030-51054-1\_29},
  doi          = {10.1007/978-3-030-51054-1\_29},
  timestamp    = {Fri, 09 Apr 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/JakubuvCOP0U20.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/mkm/UrbanJ20,
  author       = {Josef Urban and
                  Jan Jakubuv},
  editor       = {Christoph Benzm{\"{u}}ller and
                  Bruce R. Miller},
  title        = {First Neural Conjecturing Datasets and Experiments},
  booktitle    = {Intelligent Computer Mathematics - 13th International Conference,
                  {CICM} 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {12236},
  pages        = {315--323},
  publisher    = {Springer},
  year         = {2020},
  url          = {https://doi.org/10.1007/978-3-030-53518-6\_24},
  doi          = {10.1007/978-3-030-53518-6\_24},
  timestamp    = {Fri, 24 Jul 2020 13:43:13 +0200},
  biburl       = {https://dblp.org/rec/conf/mkm/UrbanJ20.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2002-05406,
  author       = {Jan Jakubuv and
                  Karel Chvalovsk{\'{y}} and
                  Miroslav Ols{\'{a}}k and
                  Bartosz Piotrowski and
                  Martin Suda and
                  Josef Urban},
  title        = {{ENIGMA} Anonymous: Symbol-Independent Inference Guiding Machine (system
                  description)},
  journal      = {CoRR},
  volume       = {abs/2002.05406},
  year         = {2020},
  url          = {https://arxiv.org/abs/2002.05406},
  eprinttype    = {arXiv},
  eprint       = {2002.05406},
  timestamp    = {Fri, 14 Feb 2020 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/corr/abs-2002-05406.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2005-14664,
  author       = {Josef Urban and
                  Jan Jakubuv},
  title        = {First Neural Conjecturing Datasets and Experiments},
  journal      = {CoRR},
  volume       = {abs/2005.14664},
  year         = {2020},
  url          = {https://arxiv.org/abs/2005.14664},
  eprinttype    = {arXiv},
  eprint       = {2005.14664},
  timestamp    = {Wed, 03 Jun 2020 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/abs-2005-14664.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/ChvalovskyJ0U19,
  author       = {Karel Chvalovsk{\'{y}} and
                  Jan Jakubuv and
                  Martin Suda and
                  Josef Urban},
  editor       = {Pascal Fontaine},
  title        = {{ENIGMA-NG:} Efficient Neural and Gradient-Boosted Inference Guidance
                  for {E}},
  booktitle    = {Automated Deduction - {CADE} 27 - 27th International Conference on
                  Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {11716},
  pages        = {197--215},
  publisher    = {Springer},
  year         = {2019},
  url          = {https://doi.org/10.1007/978-3-030-29436-6\_12},
  doi          = {10.1007/978-3-030-29436-6\_12},
  timestamp    = {Fri, 09 Apr 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/ChvalovskyJ0U19.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/JakubuvU19,
  author       = {Jan Jakubuv and
                  Josef Urban},
  editor       = {John Harrison and
                  John O'Leary and
                  Andrew Tolmach},
  title        = {Hammering Mizar by Learning Clause Guidance (Short Paper)},
  booktitle    = {10th International Conference on Interactive Theorem Proving, {ITP}
                  2019, September 9-12, 2019, Portland, OR, {USA}},
  series       = {LIPIcs},
  volume       = {141},
  pages        = {34:1--34:8},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2019},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2019.34},
  doi          = {10.4230/LIPICS.ITP.2019.34},
  timestamp    = {Sat, 07 Sep 2019 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/JakubuvU19.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tableaux/GoertzelJU19,
  author       = {Zarathustra Amadeus Goertzel and
                  Jan Jakubuv and
                  Josef Urban},
  editor       = {Serenella Cerrito and
                  Andrei Popescu},
  title        = {ENIGMAWatch: ProofWatch Meets {ENIGMA}},
  booktitle    = {Automated Reasoning with Analytic Tableaux and Related Methods - 28th
                  International Conference, {TABLEAUX} 2019, London, UK, September 3-5,
                  2019, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {11714},
  pages        = {374--388},
  publisher    = {Springer},
  year         = {2019},
  url          = {https://doi.org/10.1007/978-3-030-29026-9\_21},
  doi          = {10.1007/978-3-030-29026-9\_21},
  timestamp    = {Sat, 28 Aug 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/tableaux/GoertzelJU19.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1903-03182,
  author       = {Karel Chvalovsk{\'{y}} and
                  Jan Jakubuv and
                  Martin Suda and
                  Josef Urban},
  title        = {{ENIGMA-NG:} Efficient Neural and Gradient-Boosted Inference Guidance
                  for {E}},
  journal      = {CoRR},
  volume       = {abs/1903.03182},
  year         = {2019},
  url          = {http://arxiv.org/abs/1903.03182},
  eprinttype    = {arXiv},
  eprint       = {1903.03182},
  timestamp    = {Sun, 31 Mar 2019 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/corr/abs-1903-03182.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1904-01677,
  author       = {Jan Jakubuv and
                  Josef Urban},
  title        = {Hammering Mizar by Learning Clause Guidance},
  journal      = {CoRR},
  volume       = {abs/1904.01677},
  year         = {2019},
  url          = {http://arxiv.org/abs/1904.01677},
  eprinttype    = {arXiv},
  eprint       = {1904.01677},
  timestamp    = {Wed, 24 Apr 2019 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/abs-1904-01677.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1905-09565,
  author       = {Zarathustra Amadeus Goertzel and
                  Jan Jakubuv and
                  Josef Urban},
  title        = {ENIGMAWatch: ProofWatch Meets {ENIGMA}},
  journal      = {CoRR},
  volume       = {abs/1905.09565},
  year         = {2019},
  url          = {http://arxiv.org/abs/1905.09565},
  eprinttype    = {arXiv},
  eprint       = {1905.09565},
  timestamp    = {Sat, 28 Aug 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/abs-1905-09565.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/aicom/JakubuvU18,
  author       = {Jan Jakubuv and
                  Josef Urban},
  title        = {Hierarchical invention of theorem proving strategies},
  journal      = {{AI} Commun.},
  volume       = {31},
  number       = {3},
  pages        = {237--250},
  year         = {2018},
  url          = {https://doi.org/10.3233/AIC-180761},
  doi          = {10.3233/AIC-180761},
  timestamp    = {Wed, 23 May 2018 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/aicom/JakubuvU18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tcci/TozickaJK18,
  author       = {Jan Tozicka and
                  Jan Jakubuv and
                  Anton{\'{\i}}n Komenda},
  title        = {Recursive Reductions of Action Dependencies for Coordination-Based
                  Multiagent Planning},
  journal      = {Trans. Comput. Collect. Intell.},
  volume       = {28},
  pages        = {66--92},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-78301-7\_4},
  doi          = {10.1007/978-3-319-78301-7\_4},
  timestamp    = {Fri, 06 Mar 2020 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/tcci/TozickaJK18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icms/JakubuvK18,
  author       = {Jan Jakubuv and
                  Cezary Kaliszyk},
  editor       = {James H. Davenport and
                  Manuel Kauers and
                  George Labahn and
                  Josef Urban},
  title        = {Towards a Unified Ordering for Superposition-Based Automated Reasoning},
  booktitle    = {Mathematical Software - {ICMS} 2018 - 6th International Conference,
                  South Bend, IN, USA, July 24-27, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10931},
  pages        = {245--254},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-96418-8\_29},
  doi          = {10.1007/978-3-319-96418-8\_29},
  timestamp    = {Wed, 16 Mar 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/conf/icms/JakubuvK18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/GoertzelJ0U18,
  author       = {Zarathustra Amadeus Goertzel and
                  Jan Jakubuv and
                  Stephan Schulz and
                  Josef Urban},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {ProofWatch: Watchlist Guidance for Large Theories in {E}},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {270--288},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_16},
  doi          = {10.1007/978-3-319-94821-8\_16},
  timestamp    = {Sat, 28 Aug 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/GoertzelJ0U18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lpar/GoertzelJU18,
  author       = {Zarathustra Amadeus Goertzel and
                  Jan Jakubuv and
                  Josef Urban},
  editor       = {Gilles Barthe and
                  Konstantin Korovin and
                  Stephan Schulz and
                  Martin Suda and
                  Geoff Sutcliffe and
                  Margus Veanes},
  title        = {ProofWatch Meets {ENIGMA:} First Experiments},
  booktitle    = {{LPAR-22} Workshop and Short Paper Proceedings, Awassa, Ethiopia,
                  16-21 November 2018},
  series       = {Kalpa Publications in Computing},
  volume       = {9},
  pages        = {15--22},
  publisher    = {EasyChair},
  year         = {2018},
  url          = {https://doi.org/10.29007/z7qx},
  doi          = {10.29007/Z7QX},
  timestamp    = {Sat, 28 Aug 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/lpar/GoertzelJU18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/mkm/JakubuvU18,
  author       = {Jan Jakubuv and
                  Josef Urban},
  editor       = {Florian Rabe and
                  William M. Farmer and
                  Grant O. Passmore and
                  Abdou Youssef},
  title        = {Enhancing {ENIGMA} Given Clause Guidance},
  booktitle    = {Intelligent Computer Mathematics - 11th International Conference,
                  {CICM} 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {11006},
  pages        = {118--124},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-96812-4\_11},
  doi          = {10.1007/978-3-319-96812-4\_11},
  timestamp    = {Fri, 20 Nov 2020 16:08:55 +0100},
  biburl       = {https://dblp.org/rec/conf/mkm/JakubuvU18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1802-04007,
  author       = {Zarathustra Amadeus Goertzel and
                  Jan Jakubuv and
                  Stephan Schulz and
                  Josef Urban},
  title        = {ProofWatch: Watchlist Guidance for Large Theories in {E}},
  journal      = {CoRR},
  volume       = {abs/1802.04007},
  year         = {2018},
  url          = {http://arxiv.org/abs/1802.04007},
  eprinttype    = {arXiv},
  eprint       = {1802.04007},
  timestamp    = {Sat, 28 Aug 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/abs-1802-04007.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/JakubuvU17,
  author       = {Jan Jakubuv and
                  Josef Urban},
  editor       = {Yves Bertot and
                  Viktor Vafeiadis},
  title        = {BliStrTune: hierarchical invention of theorem proving strategies},
  booktitle    = {Proceedings of the 6th {ACM} {SIGPLAN} Conference on Certified Programs
                  and Proofs, {CPP} 2017, Paris, France, January 16-17, 2017},
  pages        = {43--52},
  publisher    = {{ACM}},
  year         = {2017},
  url          = {https://doi.org/10.1145/3018610.3018619},
  doi          = {10.1145/3018610.3018619},
  timestamp    = {Sun, 02 Jun 2019 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/cpp/JakubuvU17.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/gcai/JakubuvSU17,
  author       = {Jan Jakubuv and
                  Martin Suda and
                  Josef Urban},
  editor       = {Christoph Benzm{\"{u}}ller and
                  Christine L. Lisetti and
                  Martin Theobald},
  title        = {Automated Invention of Strategies and Term Orderings for Vampire},
  booktitle    = {{GCAI} 2017, 3rd Global Conference on Artificial Intelligence, Miami,
                  FL, USA, 18-22 October 2017},
  series       = {EPiC Series in Computing},
  volume       = {50},
  pages        = {121--133},
  publisher    = {EasyChair},
  year         = {2017},
  url          = {https://doi.org/10.29007/xghj},
  doi          = {10.29007/XGHJ},
  timestamp    = {Sun, 15 Aug 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/gcai/JakubuvSU17.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/mkm/JakubuvU17,
  author       = {Jan Jakubuv and
                  Josef Urban},
  editor       = {Herman Geuvers and
                  Matthew England and
                  Osman Hasan and
                  Florian Rabe and
                  Olaf Teschke},
  title        = {{ENIGMA:} Efficient Learning-Based Inference Guiding Machine},
  booktitle    = {Intelligent Computer Mathematics - 10th International Conference,
                  {CICM} 2017, Edinburgh, UK, July 17-21, 2017, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10383},
  pages        = {292--302},
  publisher    = {Springer},
  year         = {2017},
  url          = {https://doi.org/10.1007/978-3-319-62075-6\_20},
  doi          = {10.1007/978-3-319-62075-6\_20},
  timestamp    = {Mon, 31 Jan 2022 07:36:54 +0100},
  biburl       = {https://dblp.org/rec/conf/mkm/JakubuvU17.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/JakubuvU17,
  author       = {Jan Jakubuv and
                  Josef Urban},
  title        = {{ENIGMA:} Efficient Learning-based Inference Guiding Machine},
  journal      = {CoRR},
  volume       = {abs/1701.06532},
  year         = {2017},
  url          = {http://arxiv.org/abs/1701.06532},
  eprinttype    = {arXiv},
  eprint       = {1701.06532},
  timestamp    = {Mon, 13 Aug 2018 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/JakubuvU17.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/kais/TozickaJKP16,
  author       = {Jan Tozicka and
                  Jan Jakubuv and
                  Anton{\'{\i}}n Komenda and
                  Michal Pechoucek},
  title        = {Privacy-concerned multiagent planning},
  journal      = {Knowl. Inf. Syst.},
  volume       = {48},
  number       = {3},
  pages        = {581--618},
  year         = {2016},
  url          = {https://doi.org/10.1007/s10115-015-0887-7},
  doi          = {10.1007/S10115-015-0887-7},
  timestamp    = {Thu, 14 Oct 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/kais/TozickaJKP16.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/aips/TozickaJSK16,
  author       = {Jan Tozicka and
                  Jan Jakubuv and
                  Martin Svatos and
                  Anton{\'{\i}}n Komenda},
  editor       = {Amanda Jane Coles and
                  Andrew Coles and
                  Stefan Edelkamp and
                  Daniele Magazzeni and
                  Scott Sanner},
  title        = {Recursive Polynomial Reductions for Classical Planning},
  booktitle    = {Proceedings of the Twenty-Sixth International Conference on Automated
                  Planning and Scheduling, {ICAPS} 2016, London, UK, June 12-17, 2016},
  pages        = {317--325},
  publisher    = {{AAAI} Press},
  year         = {2016},
  url          = {http://www.aaai.org/ocs/index.php/ICAPS/ICAPS16/paper/view/13088},
  timestamp    = {Wed, 08 Jun 2016 12:49:09 +0200},
  biburl       = {https://dblp.org/rec/conf/aips/TozickaJSK16.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icaart/TozickaJK16,
  author       = {Jan Tozicka and
                  Jan Jakubuv and
                  Anton{\'{\i}}n Komenda},
  editor       = {H. Jaap van den Herik and
                  Joaquim Filipe},
  title        = {Recursive Reductions of Internal Dependencies in Multiagent Planning},
  booktitle    = {Proceedings of the 8th International Conference on Agents and Artificial
                  Intelligence {(ICAART} 2016), Volume 2, Rome, Italy, February 24-26,
                  2016},
  pages        = {181--191},
  publisher    = {SciTePress},
  year         = {2016},
  url          = {https://doi.org/10.5220/0005754901810191},
  doi          = {10.5220/0005754901810191},
  timestamp    = {Thu, 25 May 2017 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/icaart/TozickaJK16.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/mkm/JakubuvU16,
  author       = {Jan Jakubuv and
                  Josef Urban},
  editor       = {Michael Kohlhase and
                  Moa Johansson and
                  Bruce R. Miller and
                  Leonardo de Moura and
                  Frank Wm. Tompa},
  title        = {Extending {E} Prover with Similarity Based Clause Selection Strategies},
  booktitle    = {Intelligent Computer Mathematics - 9th International Conference, {CICM}
                  2016, Bialystok, Poland, July 25-29, 2016, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {9791},
  pages        = {151--156},
  publisher    = {Springer},
  year         = {2016},
  url          = {https://doi.org/10.1007/978-3-319-42547-4\_11},
  doi          = {10.1007/978-3-319-42547-4\_11},
  timestamp    = {Thu, 29 Sep 2022 08:36:57 +0200},
  biburl       = {https://dblp.org/rec/conf/mkm/JakubuvU16.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/JakubuvU16,
  author       = {Jan Jakubuv and
                  Josef Urban},
  title        = {Extending {E} Prover with Similarity Based Clause Selection Strategies},
  journal      = {CoRR},
  volume       = {abs/1606.03888},
  year         = {2016},
  url          = {http://arxiv.org/abs/1606.03888},
  eprinttype    = {arXiv},
  eprint       = {1606.03888},
  timestamp    = {Mon, 13 Aug 2018 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/JakubuvU16.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/JakubuvU16a,
  author       = {Jan Jakubuv and
                  Josef Urban},
  title        = {BliStrTune: Hierarchical Invention of Theorem Proving Strategies},
  journal      = {CoRR},
  volume       = {abs/1611.08733},
  year         = {2016},
  url          = {http://arxiv.org/abs/1611.08733},
  eprinttype    = {arXiv},
  eprint       = {1611.08733},
  timestamp    = {Mon, 13 Aug 2018 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/JakubuvU16a.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tcci/TozickaJDK15,
  author       = {Jan Tozicka and
                  Jan Jakubuv and
                  Karel Durkota and
                  Anton{\'{\i}}n Komenda},
  title        = {Extensibility Based Multiagent Planner with Plan Diversity Metrics},
  journal      = {Trans. Comput. Collect. Intell.},
  volume       = {20},
  pages        = {117--139},
  year         = {2015},
  url          = {https://doi.org/10.1007/978-3-319-27543-7\_6},
  doi          = {10.1007/978-3-319-27543-7\_6},
  timestamp    = {Fri, 06 Mar 2020 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/tcci/TozickaJDK15.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/eumas/TozickaJK15,
  author       = {Jan Tozicka and
                  Jan Jakubuv and
                  Anton{\'{\i}}n Komenda},
  editor       = {Michael Rovatsos and
                  George A. Vouros and
                  Vicente Juli{\'{a}}n},
  title        = {From Public Plans to Global Solutions in Multiagent Planning},
  booktitle    = {Multi-Agent Systems and Agreement Technologies - 13th European Conference,
                  {EUMAS} 2015, and Third International Conference, {AT} 2015, Athens,
                  Greece, December 17-18, 2015, Revised Selected Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {9571},
  pages        = {21--33},
  publisher    = {Springer},
  year         = {2015},
  url          = {https://doi.org/10.1007/978-3-319-33509-4\_2},
  doi          = {10.1007/978-3-319-33509-4\_2},
  timestamp    = {Sun, 02 Jun 2019 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/eumas/TozickaJK15.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icaart/JakubuvTK15,
  author       = {Jan Jakubuv and
                  Jan Tozicka and
                  Anton{\'{\i}}n Komenda},
  editor       = {St{\'{e}}phane Loiseau and
                  Joaquim Filipe and
                  B{\'{e}}atrice Duval and
                  H. Jaap van den Herik},
  title        = {Multiagent Planning by Plan Set Intersection and Plan Verification},
  booktitle    = {{ICAART} 2015 - Proceedings of the International Conference on Agents
                  and Artificial Intelligence, Volume 2, Lisbon, Portugal, 10-12 January,
                  2015},
  pages        = {173--182},
  publisher    = {SciTePress},
  year         = {2015},
  timestamp    = {Tue, 15 Sep 2015 09:53:57 +0200},
  biburl       = {https://dblp.org/rec/conf/icaart/JakubuvTK15.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icaart/JakubuvTK15a,
  author       = {Jan Jakubuv and
                  Jan Tozicka and
                  Anton{\'{\i}}n Komenda},
  editor       = {B{\'{e}}atrice Duval and
                  H. Jaap van den Herik and
                  St{\'{e}}phane Loiseau and
                  Joaquim Filipe},
  title        = {Using Process Calculi for Plan Verification in Multiagent Planning},
  booktitle    = {Agents and Artificial Intelligence - 7th International Conference,
                  {ICAART} 2015, Lisbon, Portugal, January 10-12, 2015, Revised Selected
                  Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {9494},
  pages        = {245--261},
  publisher    = {Springer},
  year         = {2015},
  url          = {https://doi.org/10.1007/978-3-319-27947-3\_13},
  doi          = {10.1007/978-3-319-27947-3\_13},
  timestamp    = {Tue, 16 Aug 2022 23:04:29 +0200},
  biburl       = {https://dblp.org/rec/conf/icaart/JakubuvTK15a.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ecai/TozickaJK14,
  author       = {Jan Tozicka and
                  Jan Jakubuv and
                  Anton{\'{\i}}n Komenda},
  editor       = {Torsten Schaub and
                  Gerhard Friedrich and
                  Barry O'Sullivan},
  title        = {Generating Multi-Agent Plans by Distributed Intersection of Finite
                  State Machines},
  booktitle    = {{ECAI} 2014 - 21st European Conference on Artificial Intelligence,
                  18-22 August 2014, Prague, Czech Republic - Including Prestigious
                  Applications of Intelligent Systems {(PAIS} 2014)},
  series       = {Frontiers in Artificial Intelligence and Applications},
  volume       = {263},
  pages        = {1111--1112},
  publisher    = {{IOS} Press},
  year         = {2014},
  url          = {https://doi.org/10.3233/978-1-61499-419-0-1111},
  doi          = {10.3233/978-1-61499-419-0-1111},
  timestamp    = {Mon, 19 Jun 2023 16:36:09 +0200},
  biburl       = {https://dblp.org/rec/conf/ecai/TozickaJK14.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icaart/TozickaJDKP14,
  author       = {Jan Tozicka and
                  Jan Jakubuv and
                  Karel Durkota and
                  Anton{\'{\i}}n Komenda and
                  Michal Pechoucek},
  editor       = {B{\'{e}}atrice Duval and
                  H. Jaap van den Herik and
                  St{\'{e}}phane Loiseau and
                  Joaquim Filipe},
  title        = {Multiagent Planning Supported by Plan Diversity Metrics and Landmark
                  Actions},
  booktitle    = {{ICAART} 2014 - Proceedings of the 6th International Conference on
                  Agents and Artificial Intelligence, Volume 1, ESEO, Angers, Loire
                  Valley, France, 6-8 March, 2014},
  pages        = {178--189},
  publisher    = {SciTePress},
  year         = {2014},
  url          = {https://doi.org/10.5220/0004918701780189},
  doi          = {10.5220/0004918701780189},
  timestamp    = {Thu, 14 Oct 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/icaart/TozickaJDKP14.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tgc/JakubuvW10,
  author       = {Jan Jakubuv and
                  J. B. Wells},
  editor       = {Martin Wirsing and
                  Martin Hofmann and
                  Axel Rauschmayer},
  title        = {Expressiveness of Generic Process Shape Types},
  booktitle    = {Trustworthly Global Computing - 5th International Symposium, {TGC}
                  2010, Munich, Germany, February 24-26, 2010, Revised Selected Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {6084},
  pages        = {103--119},
  publisher    = {Springer},
  year         = {2010},
  url          = {https://doi.org/10.1007/978-3-642-15640-3\_8},
  doi          = {10.1007/978-3-642-15640-3\_8},
  timestamp    = {Sun, 02 Jun 2019 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/tgc/JakubuvW10.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-1003-6096,
  author       = {Jan Jakubuv and
                  J. B. Wells},
  title        = {Expressiveness of Generic Process Shape Types},
  journal      = {CoRR},
  volume       = {abs/1003.6096},
  year         = {2010},
  url          = {http://arxiv.org/abs/1003.6096},
  eprinttype    = {arXiv},
  eprint       = {1003.6096},
  timestamp    = {Mon, 13 Aug 2018 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/abs-1003-6096.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
a service of  Schloss Dagstuhl - Leibniz Center for Informatics