Activities

Publications

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).
  
• 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).
  
• 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).
  

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 M. 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 M. 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 M. Manquinho
  arXiv CoRR abs/2206.08768 (2022).
  
• InvAASTCluster: On Applying Invariant-Based Program Clustering to Introductory Programming Assignments.
  Pedro Orvalho, Mikolás Janota, Vasco M. 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 M. 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 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.
  Pierre 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 M. 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 M. 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 M. 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 M. 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 M. 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).