Activities

Publications

2025

• Complete Symmetry Breaking for Finite Models.
  Marek Danco, Mikolás Janota, Michael Codish, João Jorge Araújo
  AAAI-25, Sponsored by the Association for the Advancement of Artificial Intelligence, February 25 - March 4, 2025, Philadelphia, PA, USA: 11194-11202 (2025).
  
• Breaking Symmetries in Quantified Graph Search: A Comparative Study.
  Mikolás Janota, Markus Kirchweger, Tomás Peitl, Stefan Szeider
  AAAI-25, Sponsored by the Association for the Advancement of Artificial Intelligence, February 25 - March 4, 2025, Philadelphia, PA, USA: 11246-11254 (2025).
  
• Counterexample Guided Program Repair Using Zero-Shot Learning and MaxSAT-based Fault Localization.
  Pedro Orvalho, Mikolás Janota, Vasco M. Manquinho
  AAAI-25, Sponsored by the Association for the Advancement of Artificial Intelligence, February 25 - March 4, 2025, Philadelphia, PA, USA: 649-657 (2025).
  
• Samoyeds: Accelerating MoE Models with Structured Sparsity Leveraging Sparse Tensor Cores.
  Chenpeng Wu, Qiqi Gu, Heng Shi, Jianguo Yao, Haibing Guan
  Proceedings of the Twentieth European Conference on Computer Systems, EuroSys 2025, Rotterdam, The Netherlands, 30 March 2025 - 3 April 2025: 293-310 (2025).
  
• Cube-based Isomorph-free Finite Model Finding.
  Choiwah Chow, Mikolás Janota, João Araújo
  arXiv CoRR abs/2501.08157 (2025/01).
  
• SAT-Based Techniques for Lexicographically Smallest Finite Models.
  Mikolás Janota, Choiwah Chow, João Araújo, Michael Codish, Petr Vojtechovský
  arXiv CoRR abs/2501.08206 (2025/01).
  
• First Experiments with Neural cvc5.
  Jelle Piepenbrock, Mikolás Janota, Jan Jakubuv
  arXiv CoRR abs/2501.09379 (2025/01).
  
• Counterexample Guided Program Repair Using Zero-Shot Learning and MaxSAT-based Fault Localization.
  Pedro Orvalho, Mikolás Janota, Vasco Manquinho
  arXiv CoRR abs/2502.07786 (2025/02).
  
• Breaking Symmetries from a Set-Covering Perspective.
  Michael Codish, Mikolás Janota
  arXiv CoRR abs/2502.10056 (2025/02).
  
• Complete Symmetry Breaking for Finite Models.
  Marek Danco, Mikolás Janota, Michael Codish, João Araújo
  arXiv CoRR abs/2502.10155 (2025/02).
  
• Breaking Symmetries in Quantified Graph Search: A Comparative Study.
  Mikolás Janota, Markus Kirchweger, Tomás Peitl, Stefan Szeider
  arXiv CoRR abs/2502.15078 (2025/02).
  
• Samoyeds: Accelerating MoE Models with Structured Sparsity Leveraging Sparse Tensor Cores.
  Chenpeng Wu, Qiqi Gu, Heng Shi, Jianguo Yao, Haibing Guan
  arXiv CoRR abs/2503.10725 (2025/03).
  
• Towards Learning Infinite SMT Models (Work in Progress).
  Mikolás Janota, Bartosz Piotrowski, Karel Chvalovský
  arXiv CoRR abs/2503.16982 (2025/03).
  
• A machine learning approach to rank pricing problems in branch-and-price.
  Pavlína Koutecká, Premysl Sucha, Jan Hula, Broos Maenhout
  Eur. J. Oper. Res. 320: 328-342 (2025).
  
• Invariant neural architecture for learning term synthesis in instantiation proving.
  Jelle Piepenbrock, Josef Urban, Konstantin Korovin, Miroslav Olsák, Tom Heskes, Mikolás Janota
  J. Symb. Comput. 128: (2025).
  

2024

• SAT-Based Techniques for Lexicographically Smallest Finite Models.
  Mikolás Janota, Choiwah Chow, João Araújo, Michael Codish, Petr Vojtechovský
  Thirty-Eighth AAAI Conference on Artificial Intelligence, AAAI 2024, Thirty-Sixth Conference on Innovative Applications of Artificial Intelligence, IAAI 2024, Fourteenth Symposium on Educational Advances in Artificial Intelligence, EAAI 2014, February 20-27, 2024, Vancouver, Canada: 8048-8056 (2024).
  
• WhyMon: A Runtime Monitoring Tool with Explanations as Verdicts.
  Leonardo Lima, Jonathan Julián Huerta y Munive, Dmitriy Traytel
  Automated Technology for Verification and Analysis - 22nd International Symposium, ATVA 2024, Kyoto, Japan, October 21-25, 2024, Proceedings, Part II: 76-90 (2024).
  
• Learning Guided Automated Reasoning: A Brief Survey.
  Lasse Blaauwbroek, David M. Cerna, Thibault Gauthier, Jan Jakubuv, Cezary Kaliszyk, Martin Suda, Josef Urban
  Logics and Type Systems in Theory and Practice - Essays Dedicated to Herman Geuvers on The Occasion of His 60th Birthday: 54-83 (2024).
  
• Understanding GNNs for Boolean Satisfiability through Approximation Algorithms.
  Jan Hula, David Mojzísek, Mikolás Janota
  Proceedings of the 33rd ACM International Conference on Information and Knowledge Management, CIKM 2024, Boise, ID, USA, October 21-25, 2024: 953-961 (2024).
  
• Cube-Based Isomorph-Free Finite Model Finding.
  Choiwah Chow, Mikolás Janota, João Araújo
  ECAI 2024 - 27th European Conference on Artificial Intelligence, 19-24 October 2024, Santiago de Compostela, Spain - Including 13th Conference on Prestigious Applications of Intelligent Systems (PAIS 2024): 4100-4107 (2024).
  
• Machine Learning for Quantifier Selection in cvc5.
  Jan Jakubuv, Mikolás Janota, Jelle Piepenbrock, Josef Urban
  ECAI 2024 - 27th European Conference on Artificial Intelligence, 19-24 October 2024, Santiago de Compostela, Spain - Including 13th Conference on Prestigious Applications of Intelligent Systems (PAIS 2024): 4336-4343 (2024).
  
• cfaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test Cases.
  Pedro Orvalho, Mikolás Janota, Vasco M. Manquinho
  Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part I: 463-481 (2024).
  
• Magnushammer: A Transformer-Based Approach to Premise Selection.
  Maciej Mikula, Szymon Tworkowski, Szymon Antoniak, Bartosz Piotrowski, Albert Q. Jiang, Jin Peng Zhou, Christian Szegedy, Lukasz Kucinski, Piotr Milos, Yuhuai Wu
  The Twelfth International Conference on Learning Representations, ICLR 2024, Vienna, Austria, May 7-11, 2024: (2024).
  
• Graph2Tac: Online Representation Learning of Formal Math Concepts.
  Lasse Blaauwbroek, Mirek Olsák, Jason Rute, Fidel Ivan Schaposnik Massolo, Jelle Piepenbrock, Vasily Pestun
  Forty-first International Conference on Machine Learning, ICML 2024, Vienna, Austria, July 21-27, 2024: (2024).
  
• Towards an Understanding of Stepwise Inference in Transformers: A Synthetic Graph Navigation Model.
  Mikail Khona, Maya Okawa, Jan Hula, Rahul Ramesh, Kento Nishi, Robert P. Dick, Ekdeep Singh Lubana, Hidenori Tanaka
  Forty-first International Conference on Machine Learning, ICML 2024, Vienna, Austria, July 21-27, 2024: (2024).
  
• Efficient Use of Large Language Models for Analysis of Text Corpora.
  David Adamczyk, Jan Hula
  Proceedings of the 13th International Conference on Pattern Recognition Applications and Methods, ICPRAM 2024, Rome, Italy, February 24-26, 2024.: 695-705 (2024).
  
• Efficient Solver Scheduling and Selection for Satisfiability Modulo Theories (SMT) Problems.
  David Mojzísek, Jan Hula
  Proceedings of the 13th International Conference on Pattern Recognition Applications and Methods, ICPRAM 2024, Rome, Italy, February 24-26, 2024.: 360-369 (2024).
  
• C-Pack of IPAs: A C90 Program Benchmark of Introductory Programming Assignments.
  Pedro Orvalho, Mikolás Janota, Vasco Manquinho
  IEEE/ACM International Workshop on Automated Program Repair, APR@ICSE 2024, Lisbon, Portugal, April 20, 2024: 14-21 (2024).
  
• Regularization in Spider-Style Strategy Discovery and Schedule Construction.
  Filip Bártek, Karel Chvalovský, Martin Suda
  Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I: 194-213 (2024).
  
• Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic.
  Johannes Niederhauser, Chad E. Brown, Cezary Kaliszyk
  Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I: 86-104 (2024).
  
• Stealing Brains: From English to Czech Language Model.
  Petr Hyner, Petr Marek, David Adamczyk, Jan Hula, Jan Sedivý
  Proceedings of the 16th International Joint Conference on Computational Intelligence, IJCCI 2024, Porto, Portugal, November 20-22, 2024.: 606-612 (2024).
  
• A Formal Proof of R(4, 5)=25.
  Thibault Gauthier, Chad E. Brown
  15th International Conference on Interactive Theorem Proving, ITP 2024, September 9-14, 2024, Tbilisi, Georgia: 16:1-16:18 (2024).
  
• Prover9 Unleashed: Automated Configuration for Enhanced Proof Discovery.
  Kristina Aleksandrova, Jan Jakubuv, Cezary Kaliszyk
  LPAR 2024: Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning, Port Louis, Mauritius, May 26-31, 2024: 360-369 (2024).
  
• First Experiments with Neural cvc5.
  Jelle Piepenbrock, Mikolas Janota, Josef Urban, Jan Jakubuv
  LPAR 2024: Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning, Port Louis, Mauritius, May 26-31, 2024: 264-277 (2024).
  
• Experiments with Choice in Dependently-Typed Higher-Order Logic.
  Daniel Ranalter, Chad E. Brown, Cezary Kaliszyk
  LPAR 2024: Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning, Port Louis, Mauritius, May 26-31, 2024: 311-320 (2024).
  
• Solving Hard Mizar Problems with Instantiation and Strategy Invention.
  Jan Jakubuv, Mikolás Janota, Josef Urban
  Intelligent Computer Mathematics - 17th International Conference, CICM 2024, Montréal, QC, Canada, August 5-9, 2024, Proceedings: 315-333 (2024).
  
• Repurposing Language Models into Embedding Models: Finding the Compute-Optimal Recipe.
  Albert Q. Jiang, Alicja Ziarko, Bartosz Piotrowski, Wenda Li, Mateja Jamnik, Piotr Milos
  Advances in Neural Information Processing Systems 38: Annual Conference on Neural Information Processing Systems 2024, NeurIPS 2024, Vancouver, BC, Canada, December 10 - 15, 2024.: (2024).
  
• Cautious Specialization of Strategy Schedules (Extended Abstract).
  Filip Bártek, Karel Chvalovský, Martin Suda
  Joint Proceedings of the 9th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 9th Satisfiability Checking and Symbolic Computation Workshop (SC-Square), 2024 co-located with the 12th International Joint Conference on Automated Reasoning (IJCAR 2024), Nancy, France, July 2, 2024.: 28-36 (2024).
  
• Symbolic Computation for All the Fun.
  Chad E. Brown, Mikolas Janota, Mirek Olsák
  Joint Proceedings of the 9th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 9th Satisfiability Checking and Symbolic Computation Workshop (SC-Square), 2024 co-located with the 12th International Joint Conference on Automated Reasoning (IJCAR 2024), Nancy, France, July 2, 2024.: 111-121 (2024).
  
• GitSEED: A Git-backed Automated Assessment Tool for Software Engineering and Programming Education.
  Pedro Orvalho, Mikolás Janota, Vasco Manquinho
  Proceedings of the 2024 ACM Virtual Global Computing Education Conference V. 1, SIGCSE Virtual 2024, Virtual Event, NC, USA, December 5-8, 2024: (2024).
  
• Explainable Online Monitoring of Metric First-Order Temporal Logic.
  Leonardo Lima, Jonathan Julián Huerta y Munive, Dmitriy Traytel
  Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I: 288-307 (2024).
  
• A Verified Proof Checker for Metric First-Order Temporal Logic.
  Andrei Herasimau, Jonathan Julián Huerta y Munive, Leonardo Lima, Martin Raszyk, Dmitriy Traytel
  Arch. Formal Proofs 2024: (2024).
  
• Graph2Tac: Learning Hierarchical Representations of Math Concepts in Theorem proving.
  Jason Rute, Miroslav Olsák, Lasse Blaauwbroek, Fidel Ivan Schaposnik Massolo, Jelle Piepenbrock, Vasily Pestun
  arXiv CoRR abs/2401.02949 (2024).
  
• Scalable Automated Verification for Cyber-Physical Systems in Isabelle/HOL.
  Jonathan Julián Huerta y Munive, Simon Foster, Mario Gleirscher, Georg Struth, Christian Pardillo Laursen, Thomas Hickman
  arXiv CoRR abs/2401.12061 (2024).
  
• Towards an Understanding of Stepwise Inference in Transformers: A Synthetic Graph Navigation Model.
  Mikail Khona, Maya Okawa, Jan Hula, Rahul Ramesh, Kento Nishi, Robert P. Dick, Ekdeep Singh Lubana, Hidenori Tanaka
  arXiv CoRR abs/2402.07757 (2024).
  
• Learning Guided Automated Reasoning: A Brief Survey.
  Lasse Blaauwbroek, David M. Cerna, Thibault Gauthier, Jan Jakubuv, Cezary Kaliszyk, Martin Suda, Josef Urban
  arXiv CoRR abs/2403.04017 (2024).
  
• Regularization in Spider-Style Strategy Discovery and Schedule Construction.
  Filip Bártek, Karel Chvalovský, Martin Suda
  arXiv CoRR abs/2403.12869 (2024).
  
• A Formal Proof of R(4, 5)=25.
  Thibault Gauthier, Chad E. Brown
  arXiv CoRR abs/2404.01761 (2024).
  
• Symbolic Computation for All the Fun.
  Chad E. Brown, Mikolás Janota, Mirek Olsák
  arXiv CoRR abs/2404.12048 (2024).
  
• Repurposing Language Models into Embedding Models: Finding the Compute-Optimal Recipe.
  Alicja Ziarko, Albert Q. Jiang, Bartosz Piotrowski, Wenda Li, Mateja Jamnik, Piotr Milos
  arXiv CoRR abs/2406.04165 (2024).
  
• Solving Hard Mizar Problems with Instantiation and Strategy Invention.
  Jan Jakubuv, Mikolás Janota, Josef Urban
  arXiv CoRR abs/2406.17762 (2024).
  
• CFaults: Model-Based Diagnosis for Fault Localization in C Programs with Multiple Test Cases.
  Pedro Orvalho, Mikolás Janota, Vasco Manquinho
  arXiv CoRR abs/2407.09337 (2024).
  
• Machine Learning for Quantifier Selection in cvc5.
  Jan Jakubuv, Mikolás Janota, Jelle Piepenbrock, Josef Urban
  arXiv CoRR abs/2408.14338 (2024).
  
• Understanding GNNs for Boolean Satisfiability through Approximation Algorithms.
  Jan Hula, David Mojzísek, Mikolás Janota
  arXiv CoRR abs/2408.15418 (2024).
  
• GitSEED: A Git-backed Automated Assessment Tool for Software Engineering and Programming Education.
  Pedro Orvalho, Mikolás Janota, Vasco Manquinho
  arXiv CoRR abs/2409.07362 (2024).
  
• Experiments with Choice in Dependently-Typed Higher-Order Logic.
  Daniel Ranalter, Chad E. Brown, Cezary Kaliszyk
  arXiv CoRR abs/2410.08874 (2024).
  
• Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic (Extended Version).
  Johannes Niederhauser, Chad E. Brown, Cezary Kaliszyk
  arXiv CoRR abs/2410.14232 (2024).
  
• Automated Strategy Invention for Confluence of Term Rewrite Systems.
  Liao Zhang, Fabian Mitterwallner, Jan Jakubuv, Cezary Kaliszyk
  arXiv CoRR abs/2411.06409 (2024).
  
• BenCzechMark : A Czech-centric Multitask and Multimetric Benchmark for Large Language Models with Duel Scoring Mechanism.
  Martin Fajcik, Martin Docekal, Jan Dolezal, Karel Ondrej, Karel Benes, Jan Kapsa, Pavel Smrz, Alexander Polok, Michal Hradis, Zuzana Neverilová, Ales Horák, Radoslav Sabol, Michal Stefánik, Adam Jirkovsky, David Adamczyk, Petr Hyner, Jan Hula, Hynek Kydlícek
  arXiv CoRR abs/2412.17933 (2024).
  
• IsaVODEs: Interactive Verification of Cyber-Physical Systems at Scale.
  Jonathan Julián Huerta y Munive, Simon Foster, Mario Gleirscher, Georg Struth, Christian Pardillo Laursen, Thomas Hickman
  J. Autom. Reason. 68: (2024/12).
  

2023

• Symmetries for Cube-And-Conquer in Finite Model Finding.
  João Araújo, Choiwah Chow, Mikolás Janota
  29th International Conference on Principles and Practice of Constraint Programming, CP 2023, August 27-31, 2023, Toronto, Canada: 8:1-8:19 (2023).
  
• Graph Neural Networks for Mapping Variables Between Programs.
  Pedro Orvalho, Jelle Piepenbrock, Mikolás Janota, Vasco Manquinho
  ECAI 2023 - 26th European Conference on Artificial Intelligence, September 30 - October 4, 2023, Kraków, Poland - Including 12th Conference on Prestigious Applications of Intelligent Systems (PAIS 2023): 1811-1818 (2023).
  
• Data-driven Single Machine Scheduling Minimizing Weighted Number of Tardy Jobs.
  Nikolai Antonov, Premysl Sucha, Mikolás Janota
  Progress in Artificial Intelligence - 22nd EPIA Conference on Artificial Intelligence, EPIA 2023, Faial Island, Azores, September 5-8, 2023, Proceedings, Part I: 483-494 (2023).
  
• The FMCAD 2023 Student Forum.
  Mikolas Janota, Nina Narodytska
  Formal Methods in Computer-Aided Design, FMCAD 2023, Ames, IA, USA, October 24-27, 2023: 1-2 (2023).
  
• Translating SUMO-K to Higher-Order Set Theory.
  Chad E. Brown, Adam Pease, Josef Urban
  Frontiers of Combining Systems - 14th International Symposium, FroCoS 2023, Prague, Czech Republic, September 20-22, 2023, Proceedings: 255-274 (2023).
  
• Fast Heuristic for Ricochet Robots.
  Jan Hula, David Adamczyk, Mikolás Janota
  Proceedings of the 15th International Conference on Agents and Artificial Intelligence, ICAART 2023, Volume 1, Lisbon, Portugal, February 22-24, 2023.: 71-79 (2023).
  
• Molecule Builder: Environment for Testing Reinforcement Learning Agents.
  Petr Hyner, Jan Hula, Mikolás Janota
  Proceedings of the 15th International Joint Conference on Computational Intelligence, IJCCI 2023, Rome, Italy, November 13-15, 2023.: 450-458 (2023).
  
• Automated Theorem Proving for Metamath.
  Mario Carneiro, Chad E. Brown, Josef Urban
  14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland: 9:1-9:19 (2023).
  
• MizAR 60 for Mizar 50.
  Jan Jakubuv, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban
  14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland: 19:1-19:22 (2023).
  
• Guiding an Instantiation Prover with Graph Neural Networks.
  Karel Chvalovský, Konstantin Korovin, Jelle Piepenbrock, Josef Urban
  LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Manizales, Colombia, 4-9th June 2023.: 112-123 (2023).
  
• A Mathematical Benchmark for Inductive Theorem Provers.
  Thibault Gauthier, Chad E. Brown, Mikolas Janota, Josef Urban
  LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Manizales, Colombia, 4-9th June 2023.: 224-237 (2023).
  
• Experiments on Infinite Model Finding in SMT Solving.
  Julian Parsert, Chad E. Brown, Mikolas Janota, Cezary Kaliszyk
  LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Manizales, Colombia, 4-9th June 2023.: 317-328 (2023).
  
• VizAR: Visualization of Automated Reasoning Proofs (System Description).
  Jan Jakubuv, Cezary Kaliszyk
  Intelligent Computer Mathematics - 16th International Conference, CICM 2023, Cambridge, UK, September 5-8, 2023, Proceedings: 303-308 (2023).
  
• Selecting Quantifiers for Instantiation in SMT.
  Jan Jakubuv, Mikolás Janota, Bartosz Piotrowski, Jelle Piepenbrock, Andrew Reynolds
  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.: 71-77 (2023).
  
• Towards Learning Infinite SMT Models (Work in Progress).
  Mikolás Janota, Bartosz Piotrowski, Karel Chvalovský
  25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2023, Nancy, France, September 11-14, 2023: 82-85 (2023).
  
• Machine-Learned Premise Selection for Lean.
  Bartosz Piotrowski, Ramon Fernández Mir, Edward W. Ayers
  Automated Reasoning with Analytic Tableaux and Related Methods - 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18-21, 2023, Proceedings: 175-186 (2023).
  
• ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics.
  Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, Jeremy Avigad
  arXiv CoRR abs/2302.12433 (2023).
  
• MizAR 60 for Mizar 50.
  Jan Jakubuv, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban
  arXiv CoRR abs/2303.06686 (2023).
  
• Machine-Learned Premise Selection for Lean.
  Bartosz Piotrowski, Ramon Fernández Mir, Edward W. Ayers
  arXiv CoRR abs/2304.00994 (2023).
  
• A Mathematical Benchmark for Inductive Theorem Provers.
  Thibault Gauthier, Chad E. Brown, Mikolas Janota, Josef Urban
  arXiv CoRR abs/2304.02986 (2023).
  
• Translating SUMO-K to Higher-Order Set Theory.
  Chad E. Brown, Adam Pease, Josef Urban
  arXiv CoRR abs/2305.07903 (2023).
  
• Graph Neural Networks For Mapping Variables Between Programs - Extended Version.
  Pedro Orvalho, Jelle Piepenbrock, Mikolás Janota, Vasco Manquinho
  arXiv CoRR abs/2307.13014 (2023).
  
• Integrated lot-sizing and scheduling: Mitigation of uncertainty in demand and processing time by machine learning.
  Mohammad Rohaninejad, Mikolás Janota, Zdenek Hanzálek
  Eng. Appl. Artif. Intell. 118: (2023).
  
• Computing generating sets of minimal size in finite algebras.
  Mikolás Janota, António Morgado, Petr Vojtechovský
  J. Symb. Comput. 119: 50-63 (2023).
  

2022

• Lash 1.0 (System Description).
  Chad E. Brown, Cezary Kaliszyk
  Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings: 350-358 (2022).
  
• Guiding an Automated Theorem Prover with Neural Rewriting.
  Jelle Piepenbrock, Tom Heskes, Mikolás Janota, Josef Urban
  Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings: 597-617 (2022).
  
• Proofgold: Blockchain for Formal Methods.
  Chad E. Brown, Cezary Kaliszyk, Thibault Gauthier, Josef Urban
  4th International Workshop on Formal Methods for Blockchains, FMBC@CAV 2022, August 11, 2022, Haifa, Israel.: 4:1-4:15 (2022).
  
• 3D Shapes Classification Using Intermediate Parts Representation.
  Jan Hula, David Mojzísek, David Adamczyk
  Information Processing and Management of Uncertainty in Knowledge-Based Systems - 19th International Conference, IPMU 2022, Milan, Italy, July 11-15, 2022, Proceedings, Part II: 431-442 (2022).
  
• Analysis of the Semantic Vector Space Induced by a Neural Language Model and a Corpus.
  Xinying Chen, Jan Hula, Antonín Dvorák
  Proceedings of the 22nd Conference Information Technologies - Applications and Theory (ITAT 2022), Zuberec, Slovakia, September 23-27, 2022.: 103-110 (2022).
  
• Image Classifier with Dynamic Set of Known Classes.
  David Mojzísek, Jan Hula
  Proceedings of the 22nd Conference Information Technologies - Applications and Theory (ITAT 2022), Zuberec, Slovakia, September 23-27, 2022.: 68-74 (2022).
  
• The Isabelle ENIGMA.
  Zarathustra Amadeus Goertzel, Jan Jakubuv, Cezary Kaliszyk, Miroslav Olsák, Jelle Piepenbrock, Josef Urban
  13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel.: 16:1-16:21 (2022).
  
• Targeted Configuration of an SMT Solver.
  Jan Hula, Jan Jakubuv, Mikolás Janota, Lukás Kubej
  Intelligent Computer Mathematics - 15th International Conference, CICM 2022, Tbilisi, Georgia, September 19-23, 2022, Proceedings: 256-271 (2022).
  
• TestSelector: Automatic Test Suite Selection for Student Projects.
  Filipe Marques, António Morgado, José Fragoso Santos, Mikolás Janota
  Runtime Verification - 22nd International Conference, RV 2022, Tbilisi, Georgia, September 28-30, 2022, Proceedings: 283-292 (2022).
  
• SAT-Based Leximax Optimisation Algorithms.
  Miguel Cabral, Mikolás Janota, Vasco Manquinho
  25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, August 2-5, 2022, Haifa, Israel.: 29:1-29:19 (2022).
  
• Towards Learning Quantifier Instantiation in SMT.
  Mikolás Janota, Jelle Piepenbrock, Bartosz Piotrowski
  25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, August 2-5, 2022, Haifa, Israel.: 7:1-7:18 (2022).
  
• MultIPAs: applying program transformations to introductory programming assignments for data augmentation.
  Pedro Orvalho, Mikolás Janota, Vasco Manquinho
  Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2022, Singapore, Singapore, November 14-18, 2022: 1657-1661 (2022).
  
• Abstract: Challenges and Solutions for Higher-Order SMT Proofs.
  Chad E. Brown, Mikolás Janota, Cezary Kaliszyk
  Proceedings of the 20th Internal Workshop on Satisfiability Modulo Theories co-located with the 11th International Joint Conference on Automated Reasoning (IJCAR 2022) part of the 8th Federated Logic Conference (FLoC 2022), Haifa, Israel, August 11-12, 2022.: (2022).
  
• Boosting isomorphic model filtering with invariants.
  João Araújo, Choiwah Chow, Mikolás Janota
  Constraints An Int. J. 27: 360-379 (2022).
  
• Boosting Isomorphic Model Filtering with Invariants.
  João Araújo, Choiwah Chow, Mikolás Janota
  arXiv CoRR abs/2201.10516 (2022).
  
• The Isabelle ENIGMA.
  Zarathustra Amadeus Goertzel, Jan Jakubuv, Cezary Kaliszyk, Miroslav Olsák, Jelle Piepenbrock, Josef Urban
  arXiv CoRR abs/2205.01981 (2022).
  
• Lash 1.0 (System Description).
  Chad E. Brown, Cezary Kaliszyk
  arXiv CoRR abs/2205.06640 (2022).
  
• C-Pack of IPAs: A C90 Program Benchmark of Introductory Programming Assignments.
  Pedro Orvalho, Mikolás Janota, Vasco Manquinho
  arXiv CoRR abs/2206.08768 (2022).
  
• InvAASTCluster: On Applying Invariant-Based Program Clustering to Introductory Programming Assignments.
  Pedro Orvalho, Mikolás Janota, Vasco Manquinho
  arXiv CoRR abs/2206.14175 (2022).
  
• TestSelector: Automatic Test Suite Selection for Student Projects - Extended Version.
  Filipe Marques, António Morgado, José Fragoso Santos, Mikolás Janota
  arXiv CoRR abs/2207.09509 (2022).
  
• Machine Learning Meets The Herbrand Universe.
  Jelle Piepenbrock, Josef Urban, Konstantin Korovin, Miroslav Olsák, Tom Heskes, Mikolas Janota
  arXiv CoRR abs/2210.03590 (2022).
  
• Poly-YOLO: higher speed, more precise detection and instance segmentation for YOLOv3.
  Petr Hurtík, Vojtech Molek, Jan Hula, Marek Vajgl, Pavel Vlasánek, Tomas Nejezchleba
  Neural Comput. Appl. 34: 8275-8290 (2022).
  
• Binary cross-entropy with dynamical clipping.
  Petr Hurtík, Stefania Tomasiello, Jan Hula, David Hynar
  Neural Comput. Appl. 34: 12029-12041 (2022).
  

2021

• Filtering Isomorphic Models by Invariants (Short Paper).
  João Araújo, Choiwah Chow, Mikolás Janota
  27th International Conference on Principles and Practice of Constraint Programming, CP 2021, Montpellier, France (Virtual Conference), October 25-29, 2021.: 4:1-4:9 (2021).
  
• The Seesaw Algorithm: Function Optimization Using Implicit Hitting Sets.
  Mikolás Janota, António Morgado, José Fragoso Santos, Vasco Manquinho
  27th International Conference on Principles and Practice of Constraint Programming, CP 2021, Montpellier, France (Virtual Conference), October 25-29, 2021.: 31:1-31:16 (2021).
  
• Fair and Adventurous Enumeration of Quantifier Instantiations.
  Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
  Formal Methods in Computer Aided Design, FMCAD 2021, New Haven, CT, USA, October 19-22, 2021: 256-260 (2021).
  
• Fast and Slow Enigmas and Parental Guidance.
  Zarathustra Amadeus Goertzel, Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban
  Frontiers of Combining Systems - 13th International Symposium, FroCoS 2021, Birmingham, UK, September 8-10, 2021, Proceedings: 173-191 (2021).
  
• Graph Neural Networks for Scheduling of SMT Solvers.
  Jan Hula, David Mojzísek, Mikolás Janota
  33rd IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2021, Washington, DC, USA, November 1-3, 2021: 447-451 (2021).
  
• Segmenting out Generic Objects in Monocular Videos.
  Jan Hula, David Adamczyk, David Mojzísek, Vojtech Molek
  Proceedings of the 21st Conference Information Technologies - Applications and Theory (ITAT 2021), Hotel Heľpa, Nízke Tatry and Muránska planina, Slovakia, September 24-28, 2021.: 123-129 (2021).
  
• Online Machine Learning Techniques for Coq: A Comparison.
  Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Prokop Cerný, Cezary Kaliszyk, Josef Urban
  Intelligent Computer Mathematics - 14th International Conference, CICM 2021, Timisoara, Romania, July 26-31, 2021, Proceedings: 67-83 (2021).
  
• First-Order Instantiation using Discriminating Terms.
  Chad E. Brown, Mikolás Janota
  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.: 17-22 (2021).
  
• Characteristic Subsets of SMT-LIB Benchmarks.
  Jan Jakubuv, Mikolás Janota, Andrew Reynolds
  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.: 53-63 (2021).
  
• Learning Theorem Proving Components.
  Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban
  Automated Reasoning with Analytic Tableaux and Related Methods - 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6-9, 2021, Proceedings: 266-278 (2021).
  
• Learning Equational Theorem Proving.
  Jelle Piepenbrock, Tom Heskes, Mikolás Janota, Josef Urban
  arXiv CoRR abs/2102.05547 (2021).
  
• Online Machine Learning Techniques for Coq: A Comparison.
  Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Prokop Cerný, Cezary Kaliszyk, Josef Urban
  arXiv CoRR abs/2104.05207 (2021).
  
• Fair and Adventurous Enumeration of Quantifier Instantiations.
  Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
  arXiv CoRR abs/2105.13700 (2021).
  
• Fast and Slow Enigmas and Parental Guidance.
  Zarathustra Amadeus Goertzel, Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban
  arXiv CoRR abs/2107.06750 (2021).
  
• Learning Theorem Proving Components.
  Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban
  arXiv CoRR abs/2107.10034 (2021).
  
• Quantified Boolean Formulas.
  Olaf Beyersdorff, Mikolás Janota, Florian Lonsing, Martina Seidl
  Handbook of Satisfiability - Second Edition: 1177-1221 (2021).
  

2020

• ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description).
  Jan Jakubuv, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, Josef Urban
  Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II: 448-463 (2020).
  
• Prolog Technology Reinforcement Learning Prover - (System Description).
  Zsolt Zombori, Josef Urban, Chad E. Brown
  Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II: 489-507 (2020).
  
• Exploration of neural machine translation in autoformalization of mathematics in Mizar.
  Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, Josef Urban
  Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020.: 85-98 (2020).
  
• Unsupervised Object-aware Learning from Videos.
  Jan Hula
  IEEE Third International Conference on Data Stream Mining, Processing, DSMP 2020, Lviv, Ukraine, August 21-25, 2020: 237-242 (2020).
  
• Acquiring Custom OCR System with Minimal Manual Annotation.
  Jan Hula, David Mojzísek, David Adamczyk, Radek Cech
  IEEE Third International Conference on Data Stream Mining, Processing, DSMP 2020, Lviv, Ukraine, August 21-25, 2020: 231-236 (2020).
  
• Keypoints Selection Using Evolutionary Algorithms.
  David Adamczyk, Jan Hula
  Proceedings of the 20th Conference Information Technologies - Applications and Theory (ITAT 2020), Hotel Tyrapol, Oravská Lesná, Slovakia, September 18-22, 2020.: 186-191 (2020).
  
• Stateful Premise Selection by Recurrent Neural Networks.
  Bartosz Piotrowski, Josef Urban
  LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020.: 409-422 (2020).
  
• Guiding Inferences in Connection Tableau by Recurrent Neural Networks.
  Bartosz Piotrowski, Josef Urban
  Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings: 309-314 (2020).
  
• First Neural Conjecturing Datasets and Experiments.
  Josef Urban, Jan Jakubuv
  Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings: 315-323 (2020).
  
• SAT-Based Encodings for Optimal Decision Trees with Explicit Paths.
  Mikolás Janota, António Morgado
  Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings: 501-518 (2020).
  
• ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description).
  Jan Jakubuv, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, Josef Urban
  arXiv CoRR abs/2002.05406 (2020).
  
• Prolog Technology Reinforcement Learning Prover.
  Zsolt Zombori, Josef Urban, Chad E. Brown
  arXiv CoRR abs/2004.06997 (2020).
  
• Stateful Premise Selection by Recurrent Neural Networks.
  Bartosz Piotrowski, Josef Urban
  arXiv CoRR abs/2004.08212 (2020).
  
• Poly-YOLO: higher speed, more precise detection and instance segmentation for YOLOv3.
  Petr Hurtík, Vojtech Molek, Jan Hula, Marek Vajgl, Pavel Vlasánek, Tomas Nejezchleba
  arXiv CoRR abs/2005.13243 (2020).
  
• First Neural Conjecturing Datasets and Experiments.
  Josef Urban, Jan Jakubuv
  arXiv CoRR abs/2005.14664 (2020).
  
• Relaxed Weighted Path Order in Theorem Proving.
  Jan Jakubuv, Cezary Kaliszyk
  Math. Comput. Sci. 14: 657-670 (2020).
  
• Data Preprocessing Technique for Neural Networks Based on Image Represented by a Fuzzy Function.
  Petr Hurtík, Vojtech Molek, Jan Hula
  IEEE Trans. Fuzzy Syst. 28: 1195-1204 (2020).
  

2019

• Can You Tell Me How to Get Past Sesame Street? Sentence-Level Pretraining Beyond Language Modeling.
  Alex Wang, Jan Hula, Patrick Xia, Raghavendra Pappagari, R. Thomas McCoy, Roma Patel, Najoung Kim, Ian Tenney, Yinghui Huang, Katherin Yu, Shuning Jin, Berlin Chen, Benjamin Van Durme, Edouard Grave, Ellie Pavlick, Samuel R. Bowman
  Proceedings of the 57th Conference of the Association for Computational Linguistics, ACL 2019, Florence, Italy, July 28- August 2, 2019, Volume 1: Long Papers: 4465-4476 (2019).
  
• GRUNGE: A Grand Unified ATP Challenge.
  Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban
  Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings: 123-141 (2019).
  
• ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E.
  Karel Chvalovský, Jan Jakubuv, Martin Suda, Josef Urban
  Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings: 197-215 (2019).
  
• On Unordered BDDs and Quantified Boolean Formulas.
  Mikolás Janota
  Progress in Artificial Intelligence, 19th EPIA Conference on Artificial Intelligence, EPIA 2019, Vila Real, Portugal, September 3-6, 2019, Proceedings, Part II.: 501-507 (2019).
  
• PrideMM: Second Order Model Checking for Memory Consistency Models.
  Simon Cooksey, Sarah Harris, Mark Batty, Radu Grigore, Mikolás Janota
  Formal Methods. FM 2019 International Workshops - Porto, Portugal, October 7-11, 2019, Revised Selected Papers, Part II: 507-525 (2019).
  
• Top-Down Neural Model For Formulae.
  Karel Chvalovský
  7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019: (2019).
  
• Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
  Chad E. Brown, Cezary Kaliszyk, Karol Pak
  10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA.: 9:1-9:16 (2019).
  
• Hammering Mizar by Learning Clause Guidance (Short Paper).
  Jan Jakubuv, Josef Urban
  10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA.: 34:1-34:8 (2019).
  
• A Tale of Two Set Theories.
  Chad E. Brown, Karol Pak
  Intelligent Computer Mathematics - 12th International Conference, CICM 2019, Prague, Czech Republic, July 8-12, 2019, Proceedings: 44-60 (2019).
  
• Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings
  Mikolás Janota, Inês Lynce
  Lecture Notes in Computer Science 11628 (2019).
  
• ENIGMAWatch: ProofWatch Meets ENIGMA.
  Zarathustra Amadeus Goertzel, Jan Jakubuv, Josef Urban
  Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, London, UK, September 3-5, 2019, Proceedings: 374-388 (2019).
  
• PrideMM: A Solver for Relaxed Memory Models.
  Simon Cooksey, Sarah Harris, Mark Batty, Radu Grigore, Mikolás Janota
  arXiv CoRR abs/1901.00428 (2019).
  
• GRUNGE: A Grand Unified ATP Challenge.
  Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban
  arXiv CoRR abs/1903.02539 (2019).
  
• ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E.
  Karel Chvalovský, Jan Jakubuv, Martin Suda, Josef Urban
  arXiv CoRR abs/1903.03182 (2019).
  
• Hammering Mizar by Learning Clause Guidance.
  Jan Jakubuv, Josef Urban
  arXiv CoRR abs/1904.01677 (2019).
  
• Cantor-Bernstein implies Excluded Middle.
  Cécilia Pradic, Chad E. Brown
  arXiv CoRR abs/1904.09193 (2019).
  
• Identifying collaborators in large codebases.
  Waren Long, Vadim Markovtsev, Hugo Mougard, Egor Bulychev, Jan Hula
  arXiv CoRR abs/1905.06782 (2019).
  
• Guiding Theorem Proving by Recurrent Neural Networks.
  Bartosz Piotrowski, Josef Urban
  arXiv CoRR abs/1905.07961 (2019).
  
• ENIGMAWatch: ProofWatch Meets ENIGMA.
  Zarathustra Amadeus Goertzel, Jan Jakubuv, Josef Urban
  arXiv CoRR abs/1905.09565 (2019).
  
• A Tale of Two Set Theories.
  Chad E. Brown, Karol Pak
  arXiv CoRR abs/1907.08368 (2019).
  
• Can Neural Networks Learn Symbolic Rewriting?
  Bartosz Piotrowski, Josef Urban, Chad E. Brown, Cezary Kaliszyk
  arXiv CoRR abs/1911.04873 (2019).
  
• Self-Learned Formula Synthesis in Set Theory.
  Chad E. Brown, Thibault Gauthier
  arXiv CoRR abs/1912.01525 (2019).
  
• Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar.
  Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, Josef Urban
  arXiv CoRR abs/1912.02636 (2019).
  
• AIM Loops and the AIM Conjecture.
  Chad E. Brown, Karol Pak
  Formaliz. Math. 27: 321-335 (2019).
  
• Context Specificity of Lemma. Diachronic Analysis.
  Jan Hula, Miroslav Kubát, Radek Cech, Xinying Chen, David Cíz, Katerina Pelegrinová, Jirí Milicka
  Glottometrics 45: 7-23 (2019).
  
• The Development of Context Specificity of Lemma. A Word Embeddings Approach.
  Radek Cech, Jan Hula, Miroslav Kubát, Xinying Chen, Jirí Milicka
  J. Quant. Linguistics 26: 187-204 (2019).
  
• New Resolution-Based QBF Calculi and Their Proof Complexity.
  Olaf Beyersdorff, Leroy Chew, Mikolás Janota
  ACM Trans. Comput. Theory 11: 26:1-26:42 (2019).
  

2018

• Towards Generalization in QBF Solving via Machine Learning.
  Mikolás Janota
  Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI-18), the 30th innovative Applications of Artificial Intelligence (IAAI-18), and the 8th AAAI Symposium on Educational Advances in Artificial Intelligence (EAAI-18), New Orleans, Louisiana, USA, February 2-7, 2018: 6607-6614 (2018).
  
• ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback.
  Bartosz Piotrowski, Josef Urban
  Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings: 566-574 (2018).
  
• Towards a Unified Ordering for Superposition-Based Automated Reasoning.
  Jan Jakubuv, Cezary Kaliszyk
  Mathematical Software - ICMS 2018 - 6th International Conference, South Bend, IN, USA, July 24-27, 2018, Proceedings: 245-254 (2018).
  
• Fully Automatic Classification of Flow Cytometry Data.
  Bartosz Pawel Piotrowski, Miron Bartosz Kursa
  Foundations of Intelligent Systems - 24th International Symposium, ISMIS 2018, Limassol, Cyprus, October 29-31, 2018, Proceedings: 3-12 (2018).
  
• ProofWatch: Watchlist Guidance for Large Theories in E.
  Zarathustra Amadeus Goertzel, Jan Jakubuv, Stephan Schulz, Josef Urban
  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: 270-288 (2018).
  
• ProofWatch Meets ENIGMA: First Experiments.
  Zarathustra Amadeus Goertzel, Jan Jakubuv, Josef Urban
  LPAR-22 Workshop and Short Paper Proceedings, Awassa, Ethiopia, 16-21 November 2018: 15-22 (2018).
  
• Towards Smarter MACE-style Model Finders.
  Mikolas Janota, Martin Suda
  LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16-21 November 2018: 454-470 (2018).
  
• Enhancing ENIGMA Given Clause Guidance.
  Jan Jakubuv, Josef Urban
  Intelligent Computer Mathematics - 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings: 118-124 (2018).
  
• Circuit-Based Search Space Pruning in QBF.
  Mikolás Janota
  Theory and Applications of Satisfiability Testing - SAT 2018 - 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings: 187-198 (2018).
  
• Hierarchical invention of theorem proving strategies.
  Jan Jakubuv, Josef Urban
  AI Commun. 31: 237-250 (2018).
  
• ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback.
  Bartosz Piotrowski, Josef Urban
  arXiv CoRR abs/1802.03375 (2018).
  
• ProofWatch: Watchlist Guidance for Large Theories in E.
  Zarathustra Amadeus Goertzel, Jan Jakubuv, Stephan Schulz, Josef Urban
  arXiv CoRR abs/1802.04007 (2018).
  
• Looking for ELMo's friends: Sentence-Level Pretraining Beyond Language Modeling.
  Samuel R. Bowman, Ellie Pavlick, Edouard Grave, Benjamin Van Durme, Alex Wang, Jan Hula, Patrick Xia, Raghavendra Pappagari, R. Thomas McCoy, Roma Patel, Najoung Kim, Ian Tenney, Yinghui Huang, Katherin Yu, Shuning Jin, Berlin Chen
  arXiv CoRR abs/1812.10860 (2018).
  
• Recursive Reductions of Action Dependencies for Coordination-Based Multiagent Planning.
  Jan Tozicka, Jan Jakubuv, Antonín Komenda
  Trans. Comput. Collect. Intell. 28: 66-92 (2018).
  

2017

• On the Quest for an Acyclic Graph.
  Mikolás Janota, Radu Grigore, Vasco Manquinho
  Proceedings of the 24th RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion 2017 co-located with the 16th International Conference of the Italian Association for Artificial Intelligence (AI*IA 2017), Bari, Italy, November 14-15, 2017.: 33-44 (2017).
  
• On Minimal Corrections in ASP.
  Mikolás Janota, João Marques-Silva
  Proceedings of the 24th RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion 2017 co-located with the 16th International Conference of the Italian Association for Artificial Intelligence (AI*IA 2017), Bari, Italy, November 14-15, 2017.: 45-54 (2017).
  
• BliStrTune: hierarchical invention of theorem proving strategies.
  Jan Jakubuv, Josef Urban
  Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017: 43-52 (2017).
  
• An Achilles' Heel of Term-Resolution.
  Mikolás Janota, João Marques-Silva
  Progress in Artificial Intelligence - 18th EPIA Conference on Artificial Intelligence, EPIA 2017, Porto, Portugal, September 5-8, 2017, Proceedings: 670-680 (2017).
  
• Automated Invention of Strategies and Term Orderings for Vampire.
  Jan Jakubuv, Martin Suda, Josef Urban
  GCAI 2017, 3rd Global Conference on Artificial Intelligence, Miami, FL, USA, 18-22 October 2017.: 121-133 (2017).
  
• Towards Visual Training Set Generation Framework.
  Jan Hula, Irina Perfilieva, Ali Ahsan Muhummad Muzaheed
  Advances in Computational Intelligence - 14th International Work-Conference on Artificial Neural Networks, IWANN 2017, Cadiz, Spain, June 14-16, 2017, Proceedings, Part II: 747-758 (2017).
  
• ENIGMA: Efficient Learning-Based Inference Guiding Machine.
  Jan Jakubuv, Josef Urban
  Intelligent Computer Mathematics - 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings: 292-302 (2017).
  
• Minimal sets on propositional formulae. Problems and reductions.
  João Marques-Silva, Mikolás Janota, Carlos Mencía
  Artif. Intell. 252: 22-50 (2017).
  
• ENIGMA: Efficient Learning-based Inference Guiding Machine.
  Jan Jakubuv, Josef Urban
  arXiv CoRR abs/1701.06532 (2017).
  
• An Achilles' Heel of Term-Resolution.
  Mikolás Janota
  arXiv CoRR abs/1704.01071 (2017).
  
• On the Quest for an Acyclic Graph.
  Mikolas Janota, Radu Grigore, Vasco Manquinho
  arXiv CoRR abs/1708.01745 (2017).
  
• QFUN: Towards Machine Learning in QBF.
  Mikolás Janota
  arXiv CoRR abs/1710.02198 (2017).
  

2016

• Extension Variables in QBF Resolution.
  Olaf Beyersdorff, Leroy Chew, Mikolas Janota
  Beyond NP, Papers from the 2016 AAAI Workshop, Phoenix, Arizona, USA, February 12, 2016.: (2016).
  
• Recursive Polynomial Reductions for Classical Planning.
  Jan Tozicka, Jan Jakubuv, Martin Svatos, Antonín Komenda
  Proceedings of the Twenty-Sixth International Conference on Automated Planning and Scheduling, ICAPS 2016, London, UK, June 12-17, 2016.: 317-325 (2016).
  
• Internal Guidance for Satallax.
  Michael Färber, Chad E. Brown
  Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings: 349-361 (2016).
  
• On Intervals and Bounds in Bit-vector Arithmetic.
  Mikolás Janota, Christoph M. Wintersteiger
  Proceedings of the 14th International Workshop on Satisfiability Modulo Theories affiliated with the International Joint Conference on Automated Reasoning, SMT@IJCAR 2016, Coimbra, Portugal, July 1-2, 2016.: 81-84 (2016).
  
• On Incremental Core-Guided MaxSAT Solving.
  Xujie Si, Xin Zhang, Vasco Manquinho, Mikolás Janota, Alexey Ignatiev, Mayur Naik
  Principles and Practice of Constraint Programming - 22nd International Conference, CP 2016, Toulouse, France, September 5-9, 2016, Proceedings: 473-482 (2016).
  
• Recursive Reductions of Internal Dependencies in Multiagent Planning.
  Jan Tozicka, Jan Jakubuv, Antonín Komenda
  Proceedings of the 8th International Conference on Agents and Artificial Intelligence (ICAART 2016), Volume 2, Rome, Italy, February 24-26, 2016.: 181-191 (2016).
  
• Extracting Higher-Order Goals from the Mizar Mathematical Library.
  Chad E. Brown, Josef Urban
  Intelligent Computer Mathematics - 9th International Conference, CICM 2016, Bialystok, Poland, July 25-29, 2016, Proceedings: 99-114 (2016).
  
• Extending E Prover with Similarity Based Clause Selection Strategies.
  Jan Jakubuv, Josef Urban
  Intelligent Computer Mathematics - 9th International Conference, CICM 2016, Bialystok, Poland, July 25-29, 2016, Proceedings: 151-156 (2016).
  
• On Q-Resolution and CDCL QBF Solving.
  Mikolás Janota
  Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings: 402-418 (2016).
  
• Solving QBF with counterexample guided refinement.
  Mikolás Janota, William Klieber, João Marques-Silva, Edmund M. Clarke
  Artif. Intell. 234: 1-25 (2016).
  
• On the query complexity of selecting minimal sets for monotone predicates.
  Mikolás Janota, João Marques-Silva
  Artif. Intell. 233: 73-83 (2016).
  
• Quantified maximum satisfiability.
  Alexey Ignatiev, Mikolás Janota, João Marques-Silva
  Constraints An Int. J. 21: 277-302 (2016).
  
• Extracting Higher-Order Goals from the Mizar Mathematical Library.
  Chad E. Brown, Josef Urban
  arXiv CoRR abs/1605.06996 (2016).
  
• Internal Guidance for Satallax.
  Michael Färber, Chad E. Brown
  arXiv CoRR abs/1605.09293 (2016).
  
• Extending E Prover with Similarity Based Clause Selection Strategies.
  Jan Jakubuv, Josef Urban
  arXiv CoRR abs/1606.03888 (2016).
  
• BliStrTune: Hierarchical Invention of Theorem Proving Strategies.
  Jan Jakubuv, Josef Urban
  arXiv CoRR abs/1611.08733 (2016).
  
• Extension Variables in QBF Resolution.
  Olaf Beyersdorff, Leroy Chew, Mikolas Janota
  informal Electron. Colloquium Comput. Complex. (2016).
  
• On Q-Resolution and CDCL QBF Solving.
  Mikolas Janota
  informal Electron. Colloquium Comput. Complex. (2016).
  
• On Exponential Lower Bounds for Partially Ordered Resolution.
  Mikolas Janota
  J. Satisf. Boolean Model. Comput. 10: 1-9 (2016).
  
• Full Lambek Calculus with Contraction is Undecidable.
  Karel Chvalovský, Rostislav Horcík
  J. Symb. Log. 81: 524-540 (2016).
  
• Privacy-concerned multiagent planning.
  Jan Tozicka, Jan Jakubuv, Antonín Komenda, Michal Pechoucek
  Knowl. Inf. Syst. 48: 581-618 (2016).
  

2015

• Efficient Extraction of QBF (Counter)models from Long-Distance Resolution Proofs.
  Valeriy Balabanov, Jie-Hong Roland Jiang, Mikolas Janota, Magdalena Widl
  Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, January 25-30, 2015, Austin, Texas, USA.: 3694-3701 (2015).
  
• From Public Plans to Global Solutions in Multiagent Planning.
  Jan Tozicka, Jan Jakubuv, Antonín Komenda
  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: 21-33 (2015).
  
• Multiagent Planning by Plan Set Intersection and Plan Verification.
  Jan Jakubuv, Jan Tozicka, Antonín Komenda
  ICAART 2015 - Proceedings of the International Conference on Agents and Artificial Intelligence, Volume 2, Lisbon, Portugal, 10-12 January, 2015.: 173-182 (2015).
  
• Using Process Calculi for Plan Verification in Multiagent Planning.
  Jan Jakubuv, Jan Tozicka, Antonín Komenda
  Agents and Artificial Intelligence - 7th International Conference, ICAART 2015, Lisbon, Portugal, January 10-12, 2015, Revised Selected Papers: 245-261 (2015).
  
• Solving QBF by Clause Selection.
  Mikolás Janota, João Marques-Silva
  Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015: 325-331 (2015).
  
• Efficient Model Based Diagnosis with Maximum Satisfiability.
  João Marques-Silva, Mikolás Janota, Alexey Ignatiev, António Morgado
  Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015: 1966-1972 (2015).
  
• Playing with Quantified Satisfaction.
  Nikolaj S. Bjørner, Mikolás Janota
  20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning - Short Presentations, LPAR 2015, Suva, Fiji, November 24-28, 2015.: 15-27 (2015).
  
• On Conflicts and Strategies in QBF.
  Nikolaj S. Bjørner, Mikolás Janota, William Klieber
  20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning - Short Presentations, LPAR 2015, Suva, Fiji, November 24-28, 2015.: 28-41 (2015).
  
• Exploiting Resolution-Based Representations for MaxSAT Solving.
  Miguel Neves, Ruben Martins, Mikolás Janota, Inês Lynce, Vasco Manquinho
  Theory and Applications of Satisfiability Testing - SAT 2015 - 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings: 272-286 (2015).
  
• Proof Complexity of Resolution-based QBF Calculi.
  Olaf Beyersdorff, Leroy Chew, Mikolás Janota
  32nd International Symposium on Theoretical Aspects of Computer Science, STACS 2015, March 4-7, 2015, Garching, Germany: 76-89 (2015).
  
• Algorithms for computing backbones of propositional formulae.
  Mikolás Janota, Inês Lynce, João Marques-Silva
  AI Commun. 28: 161-177 (2015).
  
• Exploiting Resolution-based Representations for MaxSAT Solving.
  Miguel Neves, Ruben Martins, Mikolás Janota, Inês Lynce, Vasco Manquinho
  arXiv CoRR abs/1505.02405 (2015).
  
• Reconsidering Pairs and Functions as Sets.
  Chad E. Brown
  J. Autom. Reason. 55: 199-210 (2015).
  
• Undecidability of Consequence Relation in Full non-Associative Lambek Calculus.
  Karel Chvalovský
  J. Symb. Log. 80: 567-586 (2015).
  
• Extensibility Based Multiagent Planner with Plan Diversity Metrics.
  Jan Tozicka, Jan Jakubuv, Karel Durkota, Antonín Komenda
  Trans. Comput. Collect. Intell. 20: 117-139 (2015).
  
• Expansion-based QBF solving versus Q-resolution.
  Mikolás Janota, João Marques-Silva
  Theor. Comput. Sci. 577: 25-42 (2015).