Activities

Publications

2026

• Minimizing the weighted number of tardy jobs: data-driven heuristic for single-machine scheduling.
  Nikolai Antonov, Premysl Sucha, Mikolás Janota, Jan Hula
  Comput. Oper. Res. 185: (2026).
  
• Case Study: Saturations as Explicit Models in Equational Theories.
  Mikolás Janota, Michael Rawson, Stephan Schulz
  arXiv CoRR abs/2602.16324 (2026/02).
  
• Inductive Satisfiability Certification for Universal Quantifiers and Uninterpreted Function Symbols.
  Stefan Ratschan, Anggha Nugraha, Mikolás Janota, Marek Danco
  arXiv CoRR abs/2602.16335 (2026/02).
  
• Reintroducing the Second Player in EPR.
  Leroy Chew, Mikolás Janota, Miroslav Olsák, Martin Suda
  arXiv CoRR abs/2602.16410 (2026/02).
  
• Machine learning for quantifier selection in cvc5.
  Jan Jakubuv, Mikolás Janota, Jelle Piepenbrock, Josef Urban
  Int. J. Approx. Reason. 189: (2026).
  
• Neural approaches to SAT solving: Design choices and interpretability.
  David Mojzísek, Jan Hula, Ziwei Li, Ziyu Zhou, Mikolás Janota
  Int. J. Approx. Reason. 190: (2026).
  
• MENTOR: Fixing introductory programming assignments with formula-based fault localization and LLM-driven program repair.
  Pedro Orvalho, Mikolás Janota, Vasco Manquinho
  J. Syst. Softw. 234: (2026).
  

2025

• Proof Simulation via Round-based Strategy Extraction for QBF.
  Leroy Chew
  Thirty-Ninth AAAI Conference on Artificial Intelligence, Thirty-Seventh Conference on Innovative Applications of Artificial Intelligence, Fifteenth Symposium on Educational Advances in Artificial Intelligence, AAAI 2025, Philadelphia, PA, USA, February 25 - March 4, 2025: 11176-11184 (2025).
  
• Complete Symmetry Breaking for Finite Models.
  Marek Danco, Mikolás Janota, Michael Codish, João Jorge Araújo
  Thirty-Ninth AAAI Conference on Artificial Intelligence, Thirty-Seventh Conference on Innovative Applications of Artificial Intelligence, Fifteenth Symposium on Educational Advances in Artificial Intelligence, AAAI 2025, Philadelphia, PA, USA, February 25 - March 4, 2025: 11194-11202 (2025).
  
• Breaking Symmetries in Quantified Graph Search: A Comparative Study.
  Mikolás Janota, Markus Kirchweger, Tomás Peitl, Stefan Szeider
  Thirty-Ninth AAAI Conference on Artificial Intelligence, Thirty-Seventh Conference on Innovative Applications of Artificial Intelligence, Fifteenth Symposium on Educational Advances in Artificial Intelligence, AAAI 2025, Philadelphia, PA, USA, February 25 - March 4, 2025: 11246-11254 (2025).
  
• Counterexample Guided Program Repair Using Zero-Shot Learning and MaxSAT-based Fault Localization.
  Pedro Orvalho, Mikolás Janota, Vasco M. Manquinho
  Thirty-Ninth AAAI Conference on Artificial Intelligence, Thirty-Seventh Conference on Innovative Applications of Artificial Intelligence, Fifteenth Symposium on Educational Advances in Artificial Intelligence, AAAI 2025, Philadelphia, PA, USA, February 25 - March 4, 2025: 649-657 (2025).
  
• Payment Channels with Proofs.
  Chad E. Brown, Cezary Kaliszyk, Josef Urban
  7th International Conference on Blockchain Computing and Applications, BCCA 2025, Durbovnic, Croatia, October 14-17, 2025: 271-277 (2025).
  
• SMT and Functional Equation Solving over the Reals: Challenges from the IMO.
  Chad E. Brown, Karel Chvalovský, Mikolás Janota, Mirek Olsák, Stefan Ratschan
  Automated Deduction - CADE 30 - 30th International Conference on Automated Deduction, Stuttgart, Germany, July 28-31, 2025, Proceedings: 150-163 (2025).
  
• The Vampire Diary.
  Filip Bártek, Ahmed Bhayat, Robin Coutelier, Márton Hajdú, Matthias Hetzenberger, Petra Hozzová, Laura Kovács, Jakob Rath, Michael Rawson, Giles Reger, Martin Suda, Johannes Schoisswohl, Andrei Voronkov
  Computer Aided Verification - 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part III: 57-71 (2025).
  
• Breaking Symmetries with Involutions.
  Michael Codish, Mikolás Janota
  31st International Conference on Principles and Practice of Constraint Programming, CP 2025, Glasgow, Scotland, August 10-15, 2025: 8:1-8:17 (2025).
  
• An Expansion-Based Approach for Quantified Integer Programming.
  Michael Hartisch, Leroy Chew
  31st International Conference on Principles and Practice of Constraint Programming, CP 2025, Glasgow, Scotland, August 10-15, 2025: 12:1-12:26 (2025).
  
• Breaking Symmetries from a Set-Covering Perspective.
  Michael Codish, Mikolás Janota
  Integration of Constraint Programming, Artificial Intelligence, and Operations Research - 22nd International Conference, CPAIOR 2025, Melbourne, VIC, Australia, November 10-13, 2025, Proceedings, Part I: 169-187 (2025).
  
• Synthesiz3 This: an SMT-Based Approach for Synthesis with Uncomputable Symbols.
  Petra Hozzová, Nikolaj Bjørner
  Proceedings of the 25th Conference on Formal Methods in Computer-Aided Design, FMCAD 2025, Menlo Park, CA, USA, October 6-10, 2025: (2025).
  
• The Burden of Proof: Automated Tooling for Rapid Iteration on Large Mechanised Proofs.
  Chengsong Tan, Alastair F. Donaldson, Jonathan Julián Huerta y Munive, John Wickerson
  13th IEEE/ACM International Conference on Formal Methods in Software Engineering, FormaliSE@ICSE 2025, Ottawa, ON, Canada, April 27-28, 2025: 34-45 (2025).
  
• Automated Strategy Invention for Confluence of Term Rewrite Systems.
  Liao Zhang, Fabian Mitterwallner, Jan Jakubuv, Cezary Kaliszyk
  Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2025, Montreal, Canada, August 16-22, 2025: 4724-4732 (2025).
  
• Hammering Higher Order Set Theory.
  Chad E. Brown, Cezary Kaliszyk, Martin Suda, Josef Urban
  Intelligent Computer Mathematics - 18th International Conference, CICM 2025, Brasilia, Brazil, October 6-10, 2025, Proceedings: 3-20 (2025).
  
• Exploring Formal Math on the Blockchain: An Explorer for Proofgold.
  Chad E. Brown, Cezary Kaliszyk, Josef Urban
  Intelligent Computer Mathematics - 18th International Conference, CICM 2025, Brasilia, Brazil, October 6-10, 2025, Proceedings: 71-90 (2025).
  
• Synthesis Benchmarks for Automated Reasoning.
  Márton Hajdú, Petra Hozzová, Laura Kovács, Andrei Voronkov, Eva Maria Wagner, Richard Steven Zilincík
  Intelligent Computer Mathematics - 18th International Conference, CICM 2025, Brasilia, Brazil, October 6-10, 2025, Proceedings: 21-28 (2025).
  
• Better Extension Variables in DQBF via Independence.
  Leroy Chew, Tomás Peitl
  28th International Conference on Theory and Applications of Satisfiability Testing, SAT 2025, Glasgow, Scotland, August 12-15, 2025: 11:1-11:24 (2025).
  
• Vampire. (Version 4.9)
  Filip Bártek, Ahmed Bhayat, Robin Coutelier, Márton Hajdú, Matthias Hetzenberger, Petra Hozzová, Laura Kovács, Jakob Rath, Michael Rawson, Giles Reger, Johannes Schoisswohl, Martin Suda, Andrei Voronkov
  Zenodo (2025/04)
  
• Vampire. (Version 4.9 (errata 1))
  Filip Bártek, Ahmed Bhayat, Robin Coutelier, Márton Hajdú, Matthias Hetzenberger, Petra Hozzová, Laura Kovács, Jakob Rath, Michael Rawson, Giles Reger, Johannes Schoisswohl, Martin Suda, Andrei Voronkov
  Zenodo (2025/04)
  
• MichaelHartisch/EQuIPS.
  Michael Hartisch, Leroy Chew
  DROPS Artifacts (2025/08)
  
• Synthesis Benchmarks for Automated Reasoning.
  Petra Hozzová, Márton Hajdú, Laura Kovács, Eva Maria Wagner, Richard Steven Zilincík, Andrei Voronkov
  Zenodo (2025/08)
  
• 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).
  
• Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2.
  Yuri Chervonyi, Trieu H. Trinh, Miroslav Olsák, Xiaomeng Yang, Hoang Nguyen, Marcelo Menegali, Junehyuk Jung, Vikas Verma, Quoc V. Le, Thang Luong
  arXiv CoRR abs/2502.03544 (2025/02).
  
• 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).
  
• Towards Learning Infinite SMT Models (Work in Progress).
  Mikolás Janota, Bartosz Piotrowski, Karel Chvalovský
  arXiv CoRR abs/2503.16982 (2025/03).
  
• Neural Approaches to SAT Solving: Design Choices and Interpretability.
  David Mojzísek, Jan Hula, Ziwei Li, Ziyu Zhou, Mikolás Janota
  arXiv CoRR abs/2504.01173 (2025/04).
  
• Geometric Reasoning in the Embedding Space.
  Jan Hula, David Mojzísek, Jirí Janecek, David Herel, Mikolás Janota
  arXiv CoRR abs/2504.02018 (2025/04).
  
• SMT and Functional Equation Solving over the Reals: Challenges from the IMO.
  Chad E. Brown, Karel Chvalovský, Mikolás Janota, Mirek Olsák, Stefan Ratschan
  arXiv CoRR abs/2504.15645 (2025/04).
  
• Synthesiz3 This: an SMT-Based Approach for Synthesis with Uncomputable Symbols.
  Petra Hozzová, Nikolaj Bjørner
  arXiv CoRR abs/2504.16536 (2025/04).
  
• Better Extension Variables in DQBF via Independence.
  Leroy Chew, Tomás Peitl
  arXiv CoRR abs/2505.20069 (2025/05).
  
• Breaking Symmetries with Involutions.
  Michael Codish, Mikolás Janota
  arXiv CoRR abs/2506.02903 (2025/06).
  
• The Vampire Diary.
  Filip Bártek, Ahmed Bhayat, Robin Coutelier, Márton Hajdú, Matthias Hetzenberger, Petra Hozzová, Laura Kovács, Jakob Rath, Michael Rawson, Giles Reger, Martin Suda, Johannes Schoisswohl, Andrei Voronkov
  arXiv CoRR abs/2506.03030 (2025/06).
  
• An Expansion-Based Approach for Quantified Integer Programming.
  Michael Hartisch, Leroy Chew
  arXiv CoRR abs/2506.04452 (2025/06).
  
• From MBQI to Enumerative Instantiation and Back.
  Marek Danco, Petra Hozzová, Mikolás Janota
  arXiv CoRR abs/2506.22584 (2025/06).
  
• Synthesis Benchmarks for Automated Reasoning.
  Márton Hajdú, Petra Hozzová, Laura Kovács, Andrei Voronkov, Eva Maria Wagner, Richard Steven Zilincík
  arXiv CoRR abs/2507.19827 (2025/07).
  
• Minimizing the Weighted Number of Tardy Jobs: Data-Driven Heuristic for Single-Machine Scheduling.
  Nikolai Antonov, Premysl Sucha, Mikolás Janota, Jan Hula
  arXiv CoRR abs/2508.13703 (2025/08).
  
• Quantifier Instantiations: To Mimic or To Revolt?
  Jan Jakubuv, Mikolás Janota
  arXiv CoRR abs/2508.13811 (2025/08).
  
• Experimental Results for Vampire on the Equational Theories Project.
  Mikolás Janota
  arXiv CoRR abs/2508.15856 (2025/08).
  
• Hammering Higher Order Set Theory.
  Chad E. Brown, Cezary Kaliszyk, Martin Suda, Josef Urban
  arXiv CoRR abs/2509.08264 (2025/09).
  
• Exploring Formal Math on the Blockchain: An Explorer for Proofgold.
  Chad E. Brown, Cezary Kaliszyk, Josef Urban
  arXiv CoRR abs/2509.08267 (2025/09).
  
• Payment Channels with Proofs.
  Chad E. Brown, Cezary Kaliszyk, Josef Urban
  arXiv CoRR abs/2509.08268 (2025/09).
  
• Verifying Numerical Methods with Isabelle/HOL.
  Dustin Bryant, Jonathan Julián Huerta y Munive, Simon Foster
  arXiv CoRR abs/2511.20550 (2025/11).
  
• Model-Based Diagnosis with Multiple Observations: A Unified Approach for C Software and Boolean Circuits.
  Pedro Orvalho, Marta Kwiatkowska, Mikolás Janota, Vasco Manquinho
  arXiv CoRR abs/2512.02898 (2025/12).
  
• Strong (D)QBF Dependency Schemes via Pure Universal Resolution Paths.
  Leroy Chew, Tomás Peitl
  informal Electron. Colloquium Comput. Complex. (2025).
  
• Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2.
  Yuri Chervonyi, Trieu H. Trinh, Miroslav Olsák, Xiaomeng Yang, Hoang H. Nguyen, Marcelo Menegali, Junehyuk Jung, Junsu Kim, Vikas Verma, Quoc V. Le, Thang Luong
  J. Mach. Learn. Res. 26: 241:1-241:39 (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).
  
• InvAASTCluster: On Applying Invariant-Based Program Clustering to Introductory Programming Assignments.
  Pedro Orvalho, Mikolás Janota, Vasco Manquinho
  J. Syst. Softw. 230: (2025).
  
• Geometric Reasoning in the Embedding Space.
  David Mojzísek, Jan Hula, Jirí Janecek, David Herel, Mikolás Janota
  Mach. Learn. Knowl. Extr. 7: (2025).
  

2024

• Hardness of Random Reordered Encodings of Parity for Resolution and CDCL.
  Leroy Chew, Alexis de Colnet, Friedrich Slivovsky, Stefan Szeider
  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: 7978-7986 (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).
  
• Circuits, Proofs and Propositional Model Counting.
  Sravanthi Chede, Leroy Chew, Anil Shukla
  44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2024, Gandhinagar, Gujarat, India, December 16-18, 2024: 18:1-18:23 (2024).
  
• The IMO Small Challenge: Not-Too-Hard Olympiad Math Datasets for LLMs.
  Simon Frieder, Mirek Olsák, Julius Berner, Thomas Lukasiewicz
  The Second Tiny Papers Track at ICLR 2024, Tiny Papers @ ICLR 2024, Vienna, Austria, May 11, 2024: (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: 4046-4076 (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).
  
• 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).
  
• A Formal Proof of R(4, 5)=25.
  Thibault Gauthier, Chad E. Brown
  15th International Conference on Interactive Theorem Proving, ITP 2024, Tbilisi, Georgia, September 9-14, 2024: 16:1-16:18 (2024).
  
• ASP-QRAT: A Conditionally Optimal Dual Proof System for ASP.
  Leroy Chew, Alexis de Colnet, Stefan Szeider
  Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning, KR 2024, Hanoi, Vietnam. November 2-8, 2024.: (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).
  
• 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).
  
• Supplementary Material for Breaking Symmetries in Quantified Graph Search: A Comparative Study.
  Tomás Peitl, Markus Kirchweger, Mikolás Janota, Stefan Szeider
  Zenodo (2024/12)
  
• 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).
  
• Hashing Modulo Context-Sensitive α-Equivalence.
  Lasse Blaauwbroek, Miroslav Olsák, Herman Geuvers
  arXiv CoRR abs/2401.02948 (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).
  
• Hardness of Random Reordered Encodings of Parity for Resolution and CDCL.
  Leroy Chew, Alexis de Colnet, Friedrich Slivovsky, Stefan Szeider
  arXiv CoRR abs/2402.00542 (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).
  
• 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).
  
• Circuits, Proofs and Propositional Model Counting.
  Sravanthi Chede, Leroy Chew, Anil Shukla
  informal Electron. Colloquium Comput. Complex. (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).
  
• Towards Uniform Certification in QBF.
  Leroy Chew, Friedrich Slivovsky
  Log. Methods Comput. Sci. 20: (2024).
  
• Hashing Modulo Context-Sensitive 𝛼-Equivalence.
  Lasse Blaauwbroek, Miroslav Olsák, Herman Geuvers
  Proc. ACM Program. Lang. 8: 2027-2050 (2024).
  

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, Toronto, Canada, August 27-31, 2023: 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, Białystok, Poland, July 31 - August 4, 2023: 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, Białystok, Poland, July 31 - August 4, 2023: 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).
  
• Dataset of Random Reordered Encodings of Parity Problems.
  Leroy Chew, Alexis de Colnet, Friedrich Slivovsky, Stefan Szeider
  Zenodo (2023/12)
  
• Alien Coding.
  Thibault Gauthier, Miroslav Olsák, Josef Urban
  arXiv CoRR abs/2301.11479 (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).
  
• Understanding Nullstellensatz for QBFs.
  Sravanthi Chede, Leroy Chew, Balesh Kumar, Anil Shukla
  informal Electron. Colloquium Comput. Complex. (2023).
  
• Proof Simulation via Round-based Strategy Extraction for QBF.
  Leroy Chew
  informal Electron. Colloquium Comput. Complex. (2023).
  
• Alien coding.
  Thibault Gauthier, Miroslav Olsák, Josef Urban
  Int. J. Approx. Reason. 162: (2023/11).
  
• 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, Haifa, Israel, August 11, 2022: 4:1-4:15 (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, Haifa, Israel, August 7-10, 2022: 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, Haifa, Israel, August 2-5, 2022: 29:1-29:19 (2022).
  
• Relating Existing Powerful Proof Systems for QBF.
  Leroy Chew, Marijn J. H. Heule
  25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, Haifa, Israel, August 2-5, 2022: 10:1-10:22 (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, Haifa, Israel, August 2-5, 2022: 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).
  
• Towards Uniform Certification in QBF.
  Leroy Chew, Friedrich Slivovsky
  39th International Symposium on Theoretical Aspects of Computer Science, STACS 2022, Marseille, France (Virtual Conference), March 15-18, 2022: 22:1-22:23 (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).
  
• Towards Uniform Certification in QBF.
  Leroy Chew, Friedrich Slivovsky
  arXiv CoRR abs/2210.07085 (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).
  
• Learning to Solve Geometric Construction Problems from Images.
  Jaroslav Macke, Jirí Sedlár, Miroslav Olsák, Josef Urban, Josef Sivic
  Intelligent Computer Mathematics - 14th International Conference, CICM 2021, Timisoara, Romania, July 26-31, 2021, Proceedings: 167-184 (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).
  
• Planning from Pixels in Environments with Combinatorially Hard Search Spaces.
  Marco Bagatella, Miroslav Olsák, Michal Rolínek, Georg Martius
  Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021, NeurIPS 2021, December 6-14, 2021, virtual.: 24707-24718 (2021).
  
• Hardness and Optimality in QBF Proof Systems Modulo NP.
  Leroy Chew
  Theory and Applications of Satisfiability Testing - SAT 2021 - 24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings: 98-115 (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).
  
• Avoiding Monochromatic Rectangles Using Shift Patterns.
  Zhenjun Liu, Leroy Chew, Marijn J. H. Heule
  Proceedings of the Fourteenth International Symposium on Combinatorial Search, SOCS 2021, Virtual Conference [Jinan, China], July 26-30, 2021: 225-227 (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).
  
• The Role of Entropy in Guiding a Connection Prover.
  Zsolt Zombori, Josef Urban, Miroslav Olsák
  Automated Reasoning with Analytic Tableaux and Related Methods - 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6-9, 2021, Proceedings: 218-235 (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).
  
• The Role of Entropy in Guiding a Connection Prover.
  Zsolt Zombori, Josef Urban, Miroslav Olsák
  arXiv CoRR abs/2105.14706 (2021).
  
• Learning to solve geometric construction problems from images.
  Jaroslav Macke, Jirí Sedlár, Miroslav Olsák, Josef Urban, Josef Sivic
  arXiv CoRR abs/2106.14195 (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).
  
• Planning from Pixels in Environments with Combinatorially Hard Search Spaces.
  Marco Bagatella, Mirek Olsák, Michal Rolínek, Georg Martius
  arXiv CoRR abs/2110.06149 (2021).
  
• Towards Uniform Certification in QBF.
  Leroy Chew, Friedrich Slivovsky
  informal Electron. Colloquium Comput. Complex. (2021).
  
• Erratum: Equations in oligomorphic clones and the constraint satisfaction problem for ω-categorical structures.
  Libor Barto, Michael Kompatscher, Miroslav Olsák, Trung Van Pham, Michael Pinsker
  J. Math. Log. 21: (2021).
  
• Maltsev conditions for General Congruence Meet-semidistributive Algebras.
  Miroslav Olsák
  J. Symb. Log. 86: 1432-1451 (2021).
  
• Quantified Boolean Formulas.
  Olaf Beyersdorff, Mikolás Janota, Florian Lonsing, Martina Seidl
  Handbook of Satisfiability - Second Edition: 1177-1221 (2021).
  

2020

• How QBF Expansion Makes Strategy Extraction Hard.
  Leroy Chew, Judith Clymo
  Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part I: 66-82 (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).
  
• Property Invariant Embedding for Automated Reasoning.
  Miroslav Olsák, Cezary Kaliszyk, Josef Urban
  ECAI 2020 - 24th European Conference on Artificial Intelligence, 29 August-8 September 2020, Santiago de Compostela, Spain, August 29 - September 8, 2020 - Including 10th Conference on Prestigious Applications of Artificial Intelligence (PAIS 2020): 1395-1402 (2020).
  
• GeoLogic - Graphical Interactive Theorem Prover for Euclidean Geometry.
  Miroslav Olsák
  Mathematical Software - ICMS 2020 - 7th International Conference, Braunschweig, Germany, July 13-16, 2020, Proceedings: 263-271 (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).
  
• Sorting Parity Encodings by Reusing Variables.
  Leroy Chew, Marijn J. H. Heule
  Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings: 1-10 (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).
  
• GeoLogic - Graphical interactive theorem prover for Euclidean geometry.
  Miroslav Olsák
  arXiv CoRR abs/2005.03586 (2020).
  
• First Neural Conjecturing Datasets and Experiments.
  Josef Urban, Jan Jakubuv
  arXiv CoRR abs/2005.14664 (2020).
  
• ω-categorical structures avoiding height 1 identities.
  Manuel Bodirsky, Antoine Mottet, Miroslav Olsák, Jakub Oprsal, Michael Pinsker, Ross Willard
  arXiv CoRR abs/2006.12254 (2020).
  
• Avoiding Monochromatic Rectangles Using Shift Patterns.
  Zhenjun Liu, Leroy Chew, Marijn Heule
  arXiv CoRR abs/2012.12582 (2020).
  
• Relating existing powerful proof systems for QBF.
  Leroy Chew
  informal Electron. Colloquium Comput. Complex. (2020).
  
• Loop conditions for strongly connected digraphs.
  Miroslav Olsák
  Int. J. Algebra Comput. 30: 467-499 (2020).
  
• Frege Systems for Quantified Boolean Logic.
  Olaf Beyersdorff, Ilario Bonacina, Leroy Chew, Ján Pich
  J. ACM 67: 9:1-9:36 (2020).
  
• Relaxed Weighted Path Order in Theorem Proving.
  Jan Jakubuv, Cezary Kaliszyk
  Math. Comput. Sci. 14: 657-670 (2020).
  

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).
  
• Dichotomy for Symmetric Boolean PCSPs.
  Miron Ficak, Marcin Kozik, Miroslav Olsák, Szymon Stankiewicz
  46th International Colloquium on Automata, Languages, and Programming, ICALP 2019, Patras, Greece, July 9-12, 2019: 57:1-57:12 (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, Portland, OR, USA, September 9-12, 2019: 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, Portland, OR, USA, September 9-12, 2019: 34:1-34:8 (2019).
  
• Topology is relevant (in a dichotomy conjecture for infinite-domain constraint satisfaction problems).
  Manuel Bodirsky, Antoine Mottet, Miroslav Olsák, Jakub Oprsal, Michael Pinsker, Ross Willard
  34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019: 1-12 (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).
  
• Short Proofs in QBF Expansion.
  Olaf Beyersdorff, Leroy Chew, Judith Clymo, Meena Mahajan
  Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings: 19-35 (2019).
  
• The Equivalences of Refutational QRAT.
  Leroy Chew, Judith Clymo
  Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings: 100-116 (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).
  
• Topology is relevant (in the infinite-domain dichotomy conjecture for constraint satisfaction problems).
  Manuel Bodirsky, Antoine Mottet, Miroslav Olsák, Jakub Oprsal, Michael Pinsker, Ross Willard
  arXiv CoRR abs/1901.04237 (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).
  
• Dichotomy for symmetric Boolean PCSPs.
  Miron Ficak, Marcin Kozik, Miroslav Olsák, Szymon Stankiewicz
  arXiv CoRR abs/1904.12424 (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).
  
• Property Invariant Embedding for Automated Reasoning.
  Miroslav Olsák, Cezary Kaliszyk, Josef Urban
  arXiv CoRR abs/1911.12073 (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).
  
• The Equivalences of Refutational QRAT.
  Leroy Chew, Judith Clymo
  informal Electron. Colloquium Comput. Complex. (2019).
  
• How QBF Expansion Makes Strategy Extraction Hard.
  Leroy Chew, Judith Clymo
  informal Electron. Colloquium Comput. Complex. (2019).
  
• AIM Loops and the AIM Conjecture.
  Chad E. Brown, Karol Pak
  Formaliz. Math. 27: 321-335 (2019).
  
• Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF.
  Olaf Beyersdorff, Joshua Blinkhorn, Leroy Chew, Renate A. Schmidt, Martin Suda
  J. Autom. Reason. 63: 597-623 (2019).
  
• A game characterisation of tree-like Q-Resolution size.
  Olaf Beyersdorff, Leroy Chew, Karteek Sreenivasaiah
  J. Comput. Syst. Sci. 104: 82-101 (2019).
  
• Equations in oligomorphic clones and the constraint satisfaction problem for ω-categorical structures.
  Libor Barto, Michael Kompatscher, Miroslav Olsák, Van Trung Pham, Michael Pinsker
  J. Math. Log. 19: 1950010:1-1950010:31 (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).
  
• Reinforcement Learning of Theorem Proving.
  Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Miroslav Olsák
  Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montréal, Canada.: 8836-8847 (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).
  
• Reinforcement Learning of Theorem Proving.
  Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Mirek Olsák
  arXiv CoRR abs/1805.07563 (2018).
  
• Short Proofs in QBF Expansion.
  Olaf Beyersdorff, Leroy Chew, Judith Clymo, Meena Mahajan
  informal Electron. Colloquium Comput. Complex. (2018).
  
• Hardness and Optimality in QBF Proof Systems Modulo NP.
  Leroy Chew
  informal Electron. Colloquium Comput. Complex. (2018).
  
• Understanding cutting planes for QBFs.
  Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla
  Inf. Comput. 262: 141-161 (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).
  
• Are Short Proofs Narrow? QBF Resolution Is Not So Simple.
  Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla
  ACM Trans. Comput. Log. 19: 1:1-1:26 (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).
  
• The equivalence of two dichotomy conjectures for infinite domain constraint satisfaction problems.
  Libor Barto, Michael Kompatscher, Miroslav Olsák, Trung Van Pham, Michael Pinsker
  32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017: 1-12 (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).
  
• Understanding Cutting Planes for QBFs.
  Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla
  informal Electron. Colloquium Comput. Complex. (2017).
  
• Feasible Interpolation for QBF Resolution Calculi.
  Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla
  Log. Methods Comput. Sci. 13: (2017).
  
• QBF proof complexity.
  Leroy Nicholas Chew
  Thesis (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).
  
• Understanding Cutting Planes for QBFs.
  Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla
  36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016, Chennai, India, December 13-15, 2016: 40:1-40:15 (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).
  
• Lower Bounds: From Circuits to QBF Proof Systems.
  Olaf Beyersdorff, Ilario Bonacina, Leroy Chew
  Proceedings of the 2016 ACM Conference on Innovations in Theoretical Computer Science, Cambridge, MA, USA, January 14-16, 2016: 249-260 (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).
  
• Lifting QBF Resolution Calculi to DQBF.
  Olaf Beyersdorff, Leroy Chew, Renate A. Schmidt, Martin Suda
  Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings: 490-499 (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).
  
• Are Short Proofs Narrow? QBF Resolution is not Simple.
  Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla
  33rd Symposium on Theoretical Aspects of Computer Science, STACS 2016, Orléans, France, February 17-20, 2016: 15:1-15:14 (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).
  
• Equations in oligomorphic clones and the Constraint Satisfaction Problem for $ω$-categorical structures.
  Libor Barto, Michael Kompatscher, Miroslav Olsák, Michael Pinsker, Van Trung Pham
  arXiv CoRR abs/1612.07551 (2016).
  
• Feasible Interpolation for QBF Resolution Calculi.
  Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla
  arXiv CoRR abs/1611.01328 (2016).
  
• Lifting QBF Resolution Calculi to DQBF.
  Olaf Beyersdorff, Leroy Chew, Renate A. Schmidt, Martin Suda
  arXiv CoRR abs/1604.08058 (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).
  
• Lifting QBF Resolution Calculi to DQBF.
  Olaf Beyersdorff, Leroy Chew, Renate A. Schmidt, Martin Suda
  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).
  
• 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).
  
• Feasible Interpolation for QBF Resolution Calculi.
  Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla
  Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part I: 180-192 (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).
  
• A Game Characterisation of Tree-like Q-resolution Size.
  Olaf Beyersdorff, Leroy Chew, Karteek Sreenivasaiah
  Language and Automata Theory and Applications - 9th International Conference, LATA 2015, Nice, France, March 2-6, 2015, Proceedings: 486-498 (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, Garching, Germany, March 4-7, 2015: 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).
  
• Lower bounds: from circuits to QBF proof systems.
  Olaf Beyersdorff, Ilario Bonacina, Leroy Chew
  informal Electron. Colloquium Comput. Complex. (2015).
  
• Feasible Interpolation for QBF Resolution Calculi.
  Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla
  informal Electron. Colloquium Comput. Complex. (2015).
  
• Are Short Proofs Narrow? QBF Resolution is not Simple.
  Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla
  informal Electron. Colloquium Comput. Complex. (2015).
  
• Reconsidering Pairs and Functions as Sets.
  Chad E. Brown
  J. Autom. Reason. 55: 199-210 (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).