Activities

Publications

💠 The list of all publications can be downloaded in the Excel format 👍 or in the CSV format.

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).
  
• Efficient Use of Large Language Models for Analysis of Text Corpora.
  David Adamczyk, Jan Hula
  Proceedings of the 13th International Conference on Pattern Recognition Applications and Methods, ICPRAM 2024, Rome, Italy, February 24-26, 2024.: 695-705 (2024).
  
• Efficient Solver Scheduling and Selection for Satisfiability Modulo Theories (SMT) Problems.
  David Mojzísek, Jan Hula
  Proceedings of the 13th International Conference on Pattern Recognition Applications and Methods, ICPRAM 2024, Rome, Italy, February 24-26, 2024.: 360-369 (2024).
  
• SymFormer: End-to-End Symbolic Regression Using Transformer-Based Architecture.
  Martin Vastl, Jonás Kulhánek, Jirí Kubalík, Erik Derner, Robert Babuska
  IEEE Access 12: 37840-37849 (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).
  
• The Tactician's Web of Large-Scale Formal Knowledge.
  Lasse Blaauwbroek
  arXiv CoRR abs/2401.02950 (2024).
  
• Large Language Models: A Survey.
  Shervin Minaee, Tomás Mikolov, Narjes Nikzad, Meysam Chenaghlu, Richard Socher, Xavier Amatriain, Jianfeng Gao
  arXiv CoRR abs/2402.06196 (2024).
  
• Towards an Understanding of Stepwise Inference in Transformers: A Synthetic Graph Navigation Model.
  Mikail Khona, Maya Okawa, Jan Hula, Rahul Ramesh, Kento Nishi, Robert P. Dick, Ekdeep Singh Lubana, Hidenori Tanaka
  arXiv CoRR abs/2402.07757 (2024).
  
• Learning Guided Automated Reasoning: A Brief Survey.
  Lasse Blaauwbroek, David M. Cerna, Thibault Gauthier, Jan Jakubuv, Cezary Kaliszyk, Martin Suda, Josef Urban
  arXiv CoRR abs/2403.04017 (2024).
  
• Regularization in Spider-Style Strategy Discovery and Schedule Construction.
  Filip Bártek, Karel Chvalovský, Martin Suda
  arXiv CoRR abs/2403.12869 (2024).
  

2023

• Learning Program Synthesis for Integer Sequences from Scratch.
  Thibault Gauthier, Josef Urban
  Thirty-Seventh AAAI Conference on Artificial Intelligence, AAAI 2023, Thirty-Fifth Conference on Innovative Applications of Artificial Intelligence, IAAI 2023, Thirteenth Symposium on Educational Advances in Artificial Intelligence, EAAI 2023, Washington, DC, USA, February 7-14, 2023: 7670-7677 (2023).
  
• Symmetries for Cube-And-Conquer in Finite Model Finding.
  João Araújo, Choiwah Chow, Mikolás Janota
  29th International Conference on Principles and Practice of Constraint Programming, CP 2023, August 27-31, 2023, Toronto, Canada: 8:1-8:19 (2023).
  
• Preserving Semantics in Textual Adversarial Attacks.
  David Herel, Hugo Cisneros, Tomás Mikolov
  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): 1036-1043 (2023).
  
• Graph Neural Networks for Mapping Variables Between Programs.
  Pedro Orvalho, Jelle Piepenbrock, Mikolás Janota, Vasco M. 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).
  
• Frontiers of Combining Systems - 14th International Symposium, FroCoS 2023, Prague, Czech Republic, September 20-22, 2023, Proceedings
  Uli Sattler, Martin Suda
  Lecture Notes in Computer Science 14279 (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).
  
• Learning Proof Transformations and Its Applications in Interactive Theorem Proving.
  Liao Zhang, Lasse Blaauwbroek, Cezary Kaliszyk, Josef Urban
  Frontiers of Combining Systems - 14th International Symposium, FroCoS 2023, Prague, Czech Republic, September 20-22, 2023, Proceedings: 236-254 (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).
  
• Tetra-NeRF: Representing Neural Radiance Fields Using Tetrahedra.
  Jonás Kulhánek, Torsten Sattler
  IEEE/CVF International Conference on Computer Vision, ICCV 2023, Paris, France, October 1-6, 2023: 18412-18423 (2023).
  
• Molecule Builder: Environment for Testing Reinforcement Learning Agents.
  Petr Hyner, Jan Hula, Mikolás Janota
  Proceedings of the 15th International Joint Conference on Computational Intelligence, IJCCI 2023, Rome, Italy, November 13-15, 2023.: 450-458 (2023).
  
• Automated Theorem Proving for Metamath.
  Mario Carneiro, Chad E. Brown, Josef Urban
  14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland: 9:1-9:19 (2023).
  
• MizAR 60 for Mizar 50.
  Jan Jakubuv, Karel Chvalovský, Zarathustra Amadeus Goertzel, Cezary Kaliszyk, Mirek Olsák, Bartosz Piotrowski, Stephan Schulz, Martin Suda, Josef Urban
  14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland: 19:1-19:22 (2023).
  
• How Much Should This Symbol Weigh? A GNN-Advised Clause Selection.
  Filip Bártek, Martin Suda
  LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Manizales, Colombia, 4-9th June 2023.: 96-111 (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).
  
• Automated Reasoning with Analytic Tableaux and Related Methods - 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18-21, 2023, Proceedings
  Revantha Ramanayake, Josef Urban
  Lecture Notes in Computer Science 14278 (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).
  
• Toward Physically Plausible Data-Driven Models: A Novel Neural Network Approach to Symbolic Regression.
  Jirí Kubalík, Erik Derner, Robert Babuska
  IEEE Access 11: 61481-61501 (2023).
  
• Alien Coding.
  Thibault Gauthier, Miroslav Olsák, Josef Urban
  arXiv CoRR abs/2301.11479 (2023).
  
• Neural Networks for Symbolic Regression.
  Jirí Kubalík, Erik Derner, Robert Babuska
  arXiv CoRR abs/2302.00773 (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).
  
• Tetra-NeRF: Representing Neural Radiance Fields Using Tetrahedra.
  Jonás Kulhánek, Torsten Sattler
  arXiv CoRR abs/2304.09987 (2023).
  
• Translating SUMO-K to Higher-Order Set Theory.
  Chad E. Brown, Adam Pease, Josef Urban
  arXiv CoRR abs/2305.07903 (2023).
  
• Beyond the Safeguards: Exploring the Security Risks of ChatGPT.
  Erik Derner, Kristina Batistic
  arXiv CoRR abs/2305.08005 (2023).
  
• Graph Neural Networks For Mapping Variables Between Programs - Extended Version.
  Pedro Orvalho, Jelle Piepenbrock, Mikolás Janota, Vasco M. Manquinho
  arXiv CoRR abs/2307.13014 (2023).
  
• An Evaluation of GPT-4 on the ETHICS Dataset.
  Sergey Rodionov, Zarathustra Amadeus Goertzel, Ben Goertzel
  arXiv CoRR abs/2309.10492 (2023).
  
• A Vision-Guided Robotic System for Grasping Harvested Tomato Trusses in Cluttered Environments.
  Luuk van den Bent, Tomás Coleman, Robert Babuska
  arXiv CoRR abs/2309.17170 (2023).
  
• OpenCog Hyperon: A Framework for AGI at the Human Level and Beyond.
  Ben Goertzel, Vitaly Bogdanov, Michael Duncan, Deborah Duong, Zarathustra Amadeus Goertzel, Jan Horlings, Matthew Iklé, Lucius Gregory Meredith, Alexey Potapov, Andre Luiz de Senna, Hedra Seid, Andres Suarez, Adam Vandervorst, Robert Werko
  arXiv CoRR abs/2310.18318 (2023).
  
• A Security Risk Taxonomy for Large Language Models.
  Erik Derner, Kristina Batistic, Jan Zahálka, Robert Babuska
  arXiv CoRR abs/2311.11415 (2023).
  
• Simulation Limitations of Affine Cellular Automata.
  Barbora Hudcová, Jakub Krásenský
  arXiv CoRR abs/2311.14477 (2023).
  
• Trainwreck: A damaging adversarial attack on image classifiers.
  Jan Zahálka
  arXiv CoRR abs/2311.14772 (2023).
  
• Advancing State of the Art in Language Modeling.
  David Herel, Tomás Mikolov
  arXiv CoRR abs/2312.03735 (2023).
  
• Can ChatGPT Read Who You Are?
  Erik Derner, Dalibor Kucera, Nuria Oliver, Jan Zahálka
  arXiv CoRR abs/2312.16070 (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).
  
• 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).
  
• Imitrob: Imitation Learning Dataset for Training and Evaluating 6D Object Pose Estimators.
  Jirí Sedlár, Karla Stépánová, Radoslav Skoviera, Jan Kristof Behrens, Matús Tuna, Gabriela Sejnova, Josef Sivic, Robert Babuska
  IEEE Robotics Autom. Lett. 8: 2788-2795 (2023/05).
  

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).
  
• Vampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description).
  Martin Suda
  Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings: 659-667 (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).
  
• Benchmarking Learning Efficiency in Deep Reservoir Computing.
  Hugo Cisneros, Tomás Mikolov, Josef Sivic
  Conference on Lifelong Learning Agents, CoLLAs 2022, 22-24 August 2022, McGill University, Montréal, Québec, Canada.: 532-547 (2022).
  
• ViewFormer: NeRF-Free Neural Rendering from Few Images Using Transformers.
  Jonás Kulhánek, Erik Derner, Torsten Sattler, Robert Babuska
  Computer Vision - ECCV 2022 - 17th European Conference, Tel Aviv, Israel, October 23-27, 2022, Proceedings, Part XV: 198-216 (2022).
  
• Where to Look Next: Learning Viewpoint Recommendations for Informative Trajectory Planning.
  Max Lodel, Bruno Brito, Álvaro Serra-Gómez, Laura Ferranti, Robert Babuska, Javier Alonso-Mora
  2022 International Conference on Robotics and Automation, ICRA 2022, Philadelphia, PA, USA, May 23-27, 2022: 4466-4472 (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).
  
• OpenDR: An Open Toolkit for Enabling High Performance, Low Footprint Deep Learning for Robotics.
  Nikolaos Passalis, S. Pedrazzi, Robert Babuska, Wolfram Burgard, D. Dias, F. Ferro, Moncef Gabbouj, O. Green, Alexandros Iosifidis, E. Kayacan, Jens Kober, O. Michel, Nikos Nikolaidis, Paraskevi Nousi, Roel Pieters, Maria Tzelepi, Abhinav Valada, Anastasios Tefas
  IEEE/RSJ International Conference on Intelligent Robots and Systems, IROS 2022, Kyoto, Japan, October 23-27, 2022: 12479-12484 (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).
  
• Exquisitor at the Video Browser Showdown 2022.
  Omar Shahbaz Khan, Ujjwal Sharma, Björn Þór Jónsson, Dennis C. Koelma, Stevan Rudinac, Marcel Worring, Jan Zahálka
  MultiMedia Modeling - 28th International Conference, MMM 2022, Phu Quoc, Vietnam, June 6-10, 2022, Proceedings, Part II: 511-517 (2022).
  
• XQM: Search-Oriented vs. Classifier-Oriented Relevance Feedback on Mobile Phones.
  Kim I. Schild, Alexandra M. Bagi, Magnus Holm Mamsen, Omar Shahbaz Khan, Jan Zahálka, Björn Þór Jónsson
  MultiMedia Modeling - 28th International Conference, MMM 2022, Phu Quoc, Vietnam, June 6-10, 2022, Proceedings, Part II: 458-464 (2022).
  
• Reuse of Introduced Symbols in Automatic Theorem Provers (short paper).
  Michael Rawson, Martin Suda, Petra Hozzová, Giles Reger
  Proceedings of the Workshop on Practical Aspects of Automated Reasoning Co-located with the 11th International Joint Conference on Automated Reasoning (FLoC/IJCAR 2022), Haifa, Israel, August, 11 - 12, 2022.: (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).
  
• Learning Assembly Tasks in a Few Minutes by Combining Impedance Control and Residual Recurrent Reinforcement Learning.
  Padmaja Kulkarni, Jens Kober, Robert Babuska, Cosimo Della Santina
  Adv. Intell. Syst. 4: (2022).
  
• Classification of Discrete Dynamical Systems Based on Transients.
  Barbora Hudcová, Tomás Mikolov
  Artif. Life 27: 220-245 (2022/03).
  
• Emergence of Self-Reproducing Metabolisms as Recursive Algorithms in an Artificial Chemistry.
  Germán Kruszewski, Tomás Mikolov
  Artif. Life 27: 277-299 (2022/03).
  
• 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).
  
• Six Questions about 6G.
  Kimberley Parsons Trommler, Matthias Hafner, Wolfgang Kellerer, Peter Merz, Sigurd Schuster, Josef Urban, Uwe Baeder, Bertram Gunzelmann, Andreas Kornbichler
  arXiv CoRR abs/2201.12266 (2022).
  
• Program Synthesis for the OEIS.
  Thibault Gauthier
  arXiv CoRR abs/2202.11908 (2022).
  
• OpenDR: An Open Toolkit for Enabling High Performance, Low Footprint Deep Learning for Robotics.
  Nikolaos Passalis, S. Pedrazzi, Robert Babuska, Wolfram Burgard, D. Dias, F. Ferro, Moncef Gabbouj, O. Green, Alexandros Iosifidis, E. Kayacan, Jens Kober, O. Michel, Nikolaos Nikolaidis, Paraskevi Nousi, Roel Pieters, Maria Tzelepi, Abhinav Valada, Anastasios Tefas
  arXiv CoRR abs/2203.00403 (2022).
  
• Where to Look Next: Learning Viewpoint Recommendations for Informative Trajectory Planning.
  Max Lodel, Bruno Brito, Álvaro Serra-Gómez, Laura Ferranti, Robert Babuska, Javier Alonso-Mora
  arXiv CoRR abs/2203.02381 (2022).
  
• ViewFormer: NeRF-free Neural Rendering from Few Images Using Transformers.
  Jonás Kulhánek, Erik Derner, Torsten Sattler, Robert Babuska
  arXiv CoRR abs/2203.10157 (2022).
  
• PREVIEW VERSION: Six Insights into 6G: Orientation and Input for Developing Your Strategic 6G Research Plan.
  Kimberley Parsons Trommler, Matthias Hafner, Wolfgang Kellerer, Peter Merz, Sigurd Schuster, Josef Urban, Uwe Baeder, Bertram Gunzelmann, Andreas Kornbichler
  arXiv CoRR abs/2203.13094 (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).
  
• SymFormer: End-to-end symbolic regression using transformer-based architecture.
  Martin Vastl, Jonás Kulhánek, Jirí Kubalík, Erik Derner, Robert Babuska
  arXiv CoRR abs/2205.15764 (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).
  
• Emergence of Novelty in Evolutionary Algorithms.
  David Herel, Dominika Zogatova, Matej Kripner, Tomás Mikolov
  arXiv CoRR abs/2207.04857 (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).
  
• Reproducibility Companion Paper: Describing Subjective Experiment Consistency by $p$-Value P-P Plot.
  Jakub Nawala, Lucjan Janowski, Bogdan Cmiel, Krzysztof Rusek, Marc A. Kastner, Jan Zahálka
  arXiv CoRR abs/2209.00526 (2022).
  
• Imitrob: Imitation Learning Dataset for Training and Evaluating 6D Object Pose Estimators.
  Jirí Sedlár, Karla Stépánová, Matús Tuna, Radoslav Skoviera, Jan Kristof Behrens, Gabriela Sejnova, Josef Sivic, Robert Babuska
  arXiv CoRR abs/2209.07976 (2022).
  
• Benchmarking Learning Efficiency in Deep Reservoir Computing.
  Hugo Cisneros, Josef Sivic, Tomás Mikolov
  arXiv CoRR abs/2210.02549 (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).
  
• Preserving Semantics in Textual Adversarial Attacks.
  David Herel, Hugo Cisneros, Tomás Mikolov
  arXiv CoRR abs/2211.04205 (2022).
  
• A Wos Challenge Met.
  Robert Veroff
  J. Autom. Reason. 66: 565-574 (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).
  
• IROS 2021 Online in Prague [Society News].
  Libor Preucil, Robert Babuska
  IEEE Robotics Autom. Mag. 29: 108-111 (2022).
  

2021

• Proceedings of the Third International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, ARCADE@CADE 2021, Virtual Event, July 16, 2021.
  Martin Suda, Sarah Winkler
  Proceedings of the Third International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, ARCADE@CADE 2021, Virtual Event, July 16, 2021. (2021).
  
• Improving ENIGMA-style Clause Selection while Learning From History.
  Martin Suda
  Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings: 543-561 (2021).
  
• Neural Precedence Recommender.
  Filip Bártek, Martin Suda
  Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings: 525-542 (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).
  
• Vampire with a Brain Is a Good ITP Hammer.
  Martin Suda
  Frontiers of Combining Systems - 13th International Symposium, FroCoS 2021, Birmingham, UK, September 8-10, 2021, Proceedings: 192-209 (2021).
  
• Constrained Decoding for Technical Term Retention in English-Hindi MT.
  Niyati Bafna, Martin Vastl, Ondrej Bojar
  Proceedings of the 18th International Conference on Natural Language Processing (ICON 2021), National Institute of Technology Silchar, Silchar, India, December 16 - 19, 2021.: 1-6 (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).
  
• Faster Smarter Proof by Induction in Isabelle/HOL.
  Yutaka Nagashima
  Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event / Montreal, Canada, 19-27 August 2021.: 1981-1988 (2021).
  
• Language Modeling and Artificial Intelligence.
  Tomás Mikolov
  Interspeech 2021, 22nd Annual Conference of the International Speech Communication Association, Brno, Czechia, 30 August - 3 September 2021.: (2021).
  
• Guiding Robot Model Construction with Prior Features.
  Erik Derner, Jirí Kubalík, Robert Babuska
  IEEE/RSJ International Conference on Intelligent Robots and Systems, IROS 2021, Prague, Czech Republic, September 27 - Oct. 1, 2021: 7112-7118 (2021).
  
• DeepKoCo: Efficient latent planning with a task-relevant Koopman representation.
  Bas van der Heijden, Laura Ferranti, Jens Kober, Robert Babuska
  IEEE/RSJ International Conference on Intelligent Robots and Systems, IROS 2021, Prague, Czech Republic, September 27 - Oct. 1, 2021: 183-189 (2021).
  
• Inclined Quadrotor Landing using Deep Reinforcement Learning.
  Jacob E. Kooi, Robert Babuska
  IEEE/RSJ International Conference on Intelligent Robots and Systems, IROS 2021, Prague, Czech Republic, September 27 - Oct. 1, 2021: 2361-2368 (2021).
  
• Computational Hierarchy of Elementary Cellular Automata.
  Barbora Hudcová, Tomás Mikolov
  2021 Conference on Artificial Life, ALIFE 2021, online, July 19-23, 2021: (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).
  
• Impact of Interaction Strategies on User Relevance Feedback.
  Omar Shahbaz Khan, Björn Þór Jónsson, Jan Zahálka, Stevan Rudinac, Marcel Worring
  ICMR '21: International Conference on Multimedia Retrieval, Taipei, Taiwan, August 21-24, 2021: 590-598 (2021).
  
• Exquisitor at the Lifelog Search Challenge 2021: Relationships Between Semantic Classifiers.
  Omar Shahbaz Khan, Aaron Duane, Björn Þór Jónsson, Jan Zahálka, Stevan Rudinac, Marcel Worring
  Proceedings of the 4th Annual on Lifelog Search Challenge, LSC@ICMR 2021, Taipei, Taiwan, 21 August 2021: 3-6 (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).
  
• Reproducibility Companion Paper: Kalman Filter-Based Head Motion Prediction for Cloud-Based Mixed Reality.
  Serhan Gül, Sebastian Bosse, Dimitri Podborski, Thomas Schierl, Cornelius Hellge, Marc A. Kastner, Jan Zahálka
  MM '21: ACM Multimedia Conference, Virtual Event, China, October 20 - 24, 2021: 3619-3621 (2021).
  
• Reproducibility Companion Paper: Describing Subjective Experiment Consistency by p-Value P-P Plot.
  Jakub Nawala, Lucjan Janowski, Bogdan Cmiel, Krzysztof Rusek, Marc A. Kastner, Jan Zahálka
  MM '21: ACM Multimedia Conference, Virtual Event, China, October 20 - 24, 2021: 3627-3629 (2021).
  
• XQM: Interactive Learning on Mobile Phones.
  Alexandra M. Bagi, Kim I. Schild, Omar Shahbaz Khan, Jan Zahálka, Björn Þór Jónsson
  MultiMedia Modeling - 27th International Conference, MMM 2021, Prague, Czech Republic, June 22-24, 2021, Proceedings, Part II: 281-293 (2021).
  
• Exquisitor at the Video Browser Showdown 2021: Relationships Between Semantic Classifiers.
  Omar Shahbaz Khan, Björn Þór Jónsson, Mathias Dybkjær Larsen, Liam Alex Sonto Poulsen, Dennis C. Koelma, Stevan Rudinac, Marcel Worring, Jan Zahálka
  MultiMedia Modeling - 27th International Conference, MMM 2021, Prague, Czech Republic, June 22-24, 2021, Proceedings, Part II: 410-416 (2021).
  
• First-Order Instantiation using Discriminating Terms.
  Chad E. Brown, Mikolás Janota
  Proceedings of the 19th International Workshop on Satisfiability Modulo Theories co-located with 33rd International Conference on Computer Aided Verification(CAV 2021), Online (initially located in Los Angeles, USA), July 18-19, 2021.: 17-22 (2021).
  
• Characteristic Subsets of SMT-LIB Benchmarks.
  Jan Jakubuv, Mikolás Janota, Andrew Reynolds
  Proceedings of the 19th International Workshop on Satisfiability Modulo Theories co-located with 33rd International Conference on Computer Aided Verification(CAV 2021), Online (initially located in Los Angeles, USA), July 18-19, 2021.: 53-63 (2021).
  
• Learning Theorem Proving Components.
  Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban
  Automated Reasoning with Analytic Tableaux and Related Methods - 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6-9, 2021, Proceedings: 266-278 (2021).
  
• Towards Finding Longer Proofs.
  Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, Josef Urban
  Automated Reasoning with Analytic Tableaux and Related Methods - 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6-9, 2021, Proceedings: 167-186 (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).
  
• Selecting Informative Data Samples for Model Learning Through Symbolic Regression.
  Erik Derner, Jirí Kubalík, Robert Babuska
  IEEE Access 9: 14148-14158 (2021).
  
• Symbolic Regression Methods for Reinforcement Learning.
  Jirí Kubalík, Erik Derner, Jan Zegklitz, Robert Babuska
  IEEE Access 9: 139697-139711 (2021).
  
• SAT Competition 2020.
  Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda
  Artif. Intell. 301: (2021).
  
• Control of Magnetic Manipulator Using Reinforcement Learning Based on Incrementally Adapted Local Linear Models.
  Martin Brablc, Jan Zegklitz, Robert Grepl, Robert Babuska
  Complex. 2021: 6617309:1-6617309:12 (2021).
  
• A polynomial-time scheduling approach to minimise idle energy consumption: An application to an industrial furnace.
  Ondrej Benedikt, Baran Alikoc, Premysl Sucha, Sergej Celikovský, Zdenek Hanzálek
  Comput. Oper. Res. 128: (2021).
  
• Vampire With a Brain Is a Good ITP Hammer.
  Martin Suda
  arXiv CoRR abs/2102.03529 (2021).
  
• AuGPT: Dialogue with Pre-trained Language Models and Data Augmentation.
  Jonás Kulhánek, Vojtech Hudecek, Tomás Nekvinda, Ondrej Dusek
  arXiv CoRR abs/2102.05126 (2021).
  
• Learning Equational Theorem Proving.
  Jelle Piepenbrock, Tom Heskes, Mikolás Janota, Josef Urban
  arXiv CoRR abs/2102.05547 (2021).
  
• GEM: Glare or Gloom, I Can Still See You - End-to-End Multimodal Object Detector.
  Osama Mazhar, Jens Kober, Robert Babuska
  arXiv CoRR abs/2102.12319 (2021).
  
• New Techniques that Improve ENIGMA-style Clause Selection Guidance.
  Martin Suda
  arXiv CoRR abs/2102.13564 (2021).
  
• Geometry-Based Grasping of Vine Tomatoes.
  Taeke de Haan, Padmaja Kulkarni, Robert Babuska
  arXiv CoRR abs/2103.01272 (2021).
  
• Emergence of self-reproducing metabolisms as recursive algorithms in an Artificial Chemistry.
  Germán Kruszewski, Tomás Mikolov
  arXiv CoRR abs/2103.08245 (2021).
  
• Inclined Quadrotor Landing using Deep Reinforcement Learning.
  Jacob E. Kooi, Robert Babuska
  arXiv CoRR abs/2103.09043 (2021).
  
• Visualizing computation in large-scale cellular automata.
  Hugo Cisneros, Josef Sivic, Tomás Mikolov
  arXiv CoRR abs/2104.01008 (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).
  
• Computational Hierarchy of Elementary Cellular Automata.
  Barbora Hudcová, Tomás Mikolov
  arXiv CoRR abs/2108.00415 (2021).
  
• Classification of Discrete Dynamical Systems Based on Transients.
  Barbora Hudcová, Tomás Mikolov
  arXiv CoRR abs/2108.01573 (2021).
  
• Learned Provability Likelihood for Tactical Search.
  Thibault Gauthier
  Proceedings of the 9th International Symposium on Symbolic Computation in Software Science, SCSS 2021, Hagenberg, Austria, September 8-10, 2021.: 78-85 (2021).
  
• Multi-objective symbolic regression for physics-aware dynamic modeling.
  Jirí Kubalík, Erik Derner, Robert Babuska
  Expert Syst. Appl. 182: (2021).
  
• Machine Learning Guidance for Connection Tableaux.
  Michael Färber, Cezary Kaliszyk, Josef Urban
  J. Autom. Reason. 65: 287-320 (2021).
  
• TacticToe: Learning to Prove with Tactics.
  Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, Michael Norrish
  J. Autom. Reason. 65: 257-286 (2021).
  
• Visual Navigation in Real-World Indoor Environments Using End-to-End Deep Reinforcement Learning.
  Jonás Kulhánek, Erik Derner, Robert Babuska
  IEEE Robotics Autom. Lett. 6: 4345-4352 (2021).
  
• GEM: Glare or Gloom, I Can Still See You - End-to-End Multi-Modal Object Detection.
  Osama Mazhar, Robert Babuska, Jens Kober
  IEEE Robotics Autom. Lett. 6: 6321-6328 (2021).
  
• Change detection using weighted features for image-based localization.
  Erik Derner, Clara Gómez, Alejandra C. Hernández, Ramón Barber, Robert Babuska
  Robotics Auton. Syst. 135: (2021).
  
• II-20: Intelligent and pragmatic analytic categorization of image collections.
  Jan Zahálka, Marcel Worring, Jarke J. van Wijk
  IEEE Trans. Vis. Comput. Graph. 27: 422-431 (2021).
  
• Quantified Boolean Formulas.
  Olaf Beyersdorff, Mikolás Janota, Florian Lonsing, Martina Seidl
  Handbook of Satisfiability - Second Edition: 1177-1221 (2021).
  

2020

• Learning Precedences from Simple Symbol Features.
  Filip Bártek, Martin Suda
  Joint Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 5th Satisfiability Checking and Symbolic Computation Workshop (SC-Square) Workshop, 2020 co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020), Paris, France, June-July, 2020 (Virtual).: 21-33 (2020).
  
• Layered Clause Selection for Theory Reasoning - (Short Paper).
  Bernhard Gleiss, Martin Suda
  Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part I: 402-409 (2020).
  
• Layered Clause Selection for Saturation-Based Theorem Proving.
  Bernhard Gleiss, Martin Suda
  Joint Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 5th Satisfiability Checking and Symbolic Computation Workshop (SC-Square) Workshop, 2020 co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020), Paris, France, June-July, 2020 (Virtual).: 34-52 (2020).
  
• Make E Smart Again (Short Paper).
  Zarathustra Amadeus Goertzel
  Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II: 408-415 (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).
  
• 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).
  
• Interactive Learning for Multimedia at Large.
  Omar Shahbaz Khan, Björn Þór Jónsson, Stevan Rudinac, Jan Zahálka, Hanna Ragnarsdóttir, Þórhildur Þorleiksdóttir, Gylfi Þór Guðmundsson, Laurent Amsaleg, Marcel Worring
  Advances in Information Retrieval - 42nd European Conference on IR Research, ECIR 2020, Lisbon, Portugal, April 14-17, 2020, Proceedings, Part I: 495-510 (2020).
  
• Smart Induction for Isabelle/HOL (Tool Paper).
  Yutaka Nagashima
  2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, September 21-24, 2020: 245-254 (2020).
  
• Symbolic regression driven by training data and prior knowledge.
  Jirí Kubalík, Erik Derner, Robert Babuska
  GECCO '20: Genetic and Evolutionary Computation Conference, Cancún Mexico, July 8-12, 2020: 958-966 (2020).
  
• Simultaneous task allocation and motion scheduling for complex tasks executed by multiple robots.
  Jan Kristof Behrens, Karla Stépánová, Robert Babuska
  2020 IEEE International Conference on Robotics and Automation, ICRA 2020, Paris, France, May 31 - August 31, 2020: 11443-11449 (2020).
  
• Efficient Object Search Through Probability-Based Viewpoint Selection.
  Alejandra C. Hernández, Erik Derner, Clara Gómez, Ramón Barber, Robert Babuska
  IEEE/RSJ International Conference on Intelligent Robots and Systems, IROS 2020, Las Vegas, NV, USA, October 24, 2020 - January 24, 2021: 6172-6179 (2020).
  
• Visualizing computation in large-scale cellular automata.
  Hugo Cisneros, Josef Sivic, Tomás Mikolov
  2020 Conference on Artificial Life, ALIFE 2020, online, July 13-18, 2020: 239-247 (2020).
  
• Classification of Complex Systems Based on Transients.
  Barbora Hudcová, Tomás Mikolov
  2020 Conference on Artificial Life, ALIFE 2020, online, July 13-18, 2020: 367-375 (2020).
  
• Combinatory Chemistry: Towards a Simple Model of Emergent Evolution.
  Germán Kruszewski, Tomás Mikolov
  2020 Conference on Artificial Life, ALIFE 2020, online, July 13-18, 2020: 411-419 (2020).
  
• Tactile-Based Self-supervised Pose Estimation for Robust Grasping.
  Padmaja Kulkarni, Jens Kober, Robert Babuska
  Experimental Robotics - The 17th International Symposium, ISER 2020, La Valletta, Malta, November 9-12, 2020 (postponed to 2021).: 277-284 (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).
  
• Tactic Learning and Proving for the Coq Proof Assistant.
  Lasse Blaauwbroek, Josef Urban, Herman Geuvers
  LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020.: 138-150 (2020).
  
• Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic.
  Thibault Gauthier
  LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020.: 230-248 (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).
  
• Exquisitor at the Lifelog Search Challenge 2020.
  Omar Shahbaz Khan, Mathias Dybkjær Larsen, Liam Alex Sonto Poulsen, Björn Þór Jónsson, Jan Zahálka, Stevan Rudinac, Dennis C. Koelma, Marcel Worring
  Proceedings of the Third ACM Workshop on Lifelog Search Challenge, LSC@ICMR 2020, Dublin, Ireland, June 8-11, 2020.: 19-22 (2020).
  
• The Tactician - A Seamless, Interactive Tactic Learner and Prover for Coq.
  Lasse Blaauwbroek, Josef Urban, Herman Geuvers
  Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings: 271-277 (2020).
  
• Tree Neural Networks in HOL4.
  Thibault Gauthier
  Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings: 278-283 (2020).
  
• Simple Dataset for Proof Method Recommendation in Isabelle/HOL.
  Yutaka Nagashima
  Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings: 297-302 (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).
  
• Reproducibility Companion Paper: Selective Deep Convolutional Features for Image Retrieval.
  Tuan Hoang, Thanh-Toan Do, Ngai-Man Cheung, Michael Riegler, Jan Zahálka
  MM '20: The 28th ACM International Conference on Multimedia, Virtual Event / Seattle, WA, USA, October 12-16, 2020: 4448-4452 (2020).
  
• Reproducibility Companion Paper: Outfit Compatibility Prediction and Diagnosis with Multi-Layered Comparison Network.
  Xin Wang, Bo Wu, Yueqi Zhong, Wei Hu, Jan Zahálka
  MM '20: The 28th ACM International Conference on Multimedia, Virtual Event / Seattle, WA, USA, October 12-16, 2020: 4439-4443 (2020).
  
• Exquisitor at the Video Browser Showdown 2020.
  Björn Þór Jónsson, Omar Shahbaz Khan, Dennis C. Koelma, Stevan Rudinac, Marcel Worring, Jan Zahálka
  MultiMedia Modeling - 26th International Conference, MMM 2020, Daejeon, South Korea, January 5-8, 2020, Proceedings, Part II: 796-802 (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).
  
• The Effects of Adaptive Control on Learning Directed Locomotion.
  Fuda van Diggelen, Robert Babuska, A. E. Eiben
  2020 IEEE Symposium Series on Computational Intelligence, SSCI 2020, Canberra, Australia, December 1-4, 2020: 2117-2124 (2020).
  
• Constructing parsimonious analytic models for dynamic systems via symbolic regression.
  Erik Derner, Jirí Kubalík, Nicola Ancona, Robert Babuska
  Appl. Soft Comput. 94: (2020).
  
• Layered Clause Selection for Theory Reasoning.
  Bernhard Gleiss, Martin Suda
  arXiv CoRR abs/2001.09705 (2020).
  
• Smart Induction for Isabelle/HOL (System Description).
  Yutaka Nagashima
  arXiv CoRR abs/2001.10834 (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).
  
• Combinatory Chemistry: Towards a Simple Model of Emergent Evolution.
  Germán Kruszewski, Tomás Mikolov
  arXiv CoRR abs/2003.07916 (2020).
  
• Tactic Learning and Proving for the Coq Proof Assistant.
  Lasse Blaauwbroek, Josef Urban, Herman Geuvers
  arXiv CoRR abs/2003.09140 (2020).
  
• Class-Agnostic Continual Learning of Alternating Languages and Domains.
  Germán Kruszewski, Ionut-Teodor Sorodoc, Tomás Mikolov
  arXiv CoRR abs/2004.03340 (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).
  
• Make E Smart Again.
  Zarathustra Amadeus Goertzel
  arXiv CoRR abs/2004.08858 (2020).
  
• Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description).
  Yutaka Nagashima
  arXiv CoRR abs/2004.10667 (2020).
  
• Symbolic Regression Driven by Training Data and Prior Knowledge.
  Jirí Kubalík, Erik Derner, Robert Babuska
  arXiv CoRR abs/2004.11947 (2020).
  
• II-20: Intelligent and pragmatic analytic categorization of image collections.
  Jan Zahálka, Marcel Worring, Jarke J. van Wijk
  arXiv CoRR abs/2005.02149 (2020).
  
• Towards United Reasoning for Automatic Induction in Isabelle/HOL.
  Yutaka Nagashima
  arXiv CoRR abs/2005.12737 (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).
  
• An Integrated Approach to Goal Selection in Mobile Robot Exploration.
  Miroslav Kulich, Jirí Kubalík, Libor Preucil
  arXiv CoRR abs/2007.10085 (2020).
  
• The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq.
  Lasse Blaauwbroek, Josef Urban, Herman Geuvers
  arXiv CoRR abs/2008.00120 (2020).
  
• Classification of Complex Systems Based on Transients.
  Barbora Hudcová, Tomás Mikolov
  arXiv CoRR abs/2008.13503 (2020).
  
• Tree Neural Networks in HOL4.
  Thibault Gauthier
  arXiv CoRR abs/2009.01827 (2020).
  
• Faster Smarter Induction in Isabelle/HOL with SeLFiE.
  Yutaka Nagashima
  arXiv CoRR abs/2009.09215 (2020).
  
• Predicting Typological Features in WALS using Language Embeddings and Conditional Probabilities: ÚFAL Submission to the SIGTYP 2020 Shared Task.
  Martin Vastl, Daniel Zeman, Rudolf Rosa
  arXiv CoRR abs/2010.03920 (2020).
  
• SeLFiE: Modular Semantic Reasoning for Induction in Isabelle/HOL.
  Yutaka Nagashima
  arXiv CoRR abs/2010.10296 (2020).
  
• Visual Navigation in Real-World Indoor Environments Using End-to-End Deep Reinforcement Learning.
  Jonás Kulhánek, Erik Derner, Robert Babuska
  arXiv CoRR abs/2010.10903 (2020).
  
• DeepKoCo: Efficient latent planning with an invariant Koopman representation.
  Bas van der Heijden, Laura Ferranti, Jens Kober, Robert Babuska
  arXiv CoRR abs/2011.12690 (2020).
  
• Special Issue "On Defining Artificial Intelligence" - Commentaries and Author's Response.
  Dagmar Monett, Colin W. P. Lewis, Kristinn R. Thórisson, Joscha Bach, Gianluca Baldassarre, Giovanni Granato, Istvan S. N. Berkeley, François Chollet, Matthew Crosby, Henry Shevlin, John F. Sowa, John E. Laird, Shane Legg, Peter Lindes, Tomás Mikolov, William J. Rapaport, Raúl Rojas, Marek Rosa, Peter Stone, Richard S. Sutton, Roman V. Yampolskiy, Pei Wang, Roger C. Schank, Aaron Sloman, Alan F. T. Winfield
  J. Artif. Gen. Intell. 11: 1-100 (2020).
  
• Relaxed Weighted Path Order in Theorem Proving.
  Jan Jakubuv, Cezary Kaliszyk
  Math. Comput. Sci. 14: 657-670 (2020).
  
• Foreword.
  George Labahn, James H. Davenport, Josef Urban
  Math. Comput. Sci. 14: 531-532 (2020).
  
• Object-Based Pose Graph for Dynamic Indoor Environments.
  Clara Gómez, Alejandra C. Hernández, Erik Derner, Ramón Barber, Robert Babuska
  IEEE Robotics Autom. Lett. 5: 5401-5408 (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).
  
• LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL.
  Yutaka Nagashima
  Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings: 266-287 (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).
  
• Towards Life-Long Autonomy of Mobile Robots Through Feature-Based Change Detection.
  Erik Derner, Clara Gómez, Alejandra C. Hernández, Ramón Barber, Robert Babuska
  2019 European Conference on Mobile Robots, ECMR 2019, Prague, Czech Republic, September 4-6, 2019: 1-6 (2019).
  
• Semantic Localization through Propagation of Scene Information in a Hierarchical Model.
  Clara Gómez, Alejandra C. Hernández, Erik Derner, Ramón Barber
  2019 European Conference on Mobile Robots, ECMR 2019, Prague, Czech Republic, September 4-6, 2019: 1-6 (2019).
  
• Indoor Scene Recognition based on Weighted Voting Schemes.
  Alejandra C. Hernández, Clara Gómez, Erik Derner, Ramón Barber
  2019 European Conference on Mobile Robots, ECMR 2019, Prague, Czech Republic, September 4-6, 2019: 1-6 (2019).
  
• Vision-based Navigation Using Deep Reinforcement Learning.
  Jonás Kulhánek, Erik Derner, Tim de Bruin, Robert Babuska
  2019 European Conference on Mobile Robots, ECMR 2019, Prague, Czech Republic, September 4-6, 2019: 1-8 (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).
  
• Symmetry Avoidance in MACE-Style Finite Model Finding.
  Giles Reger, Martin Riener, Martin Suda
  Frontiers of Combining Systems - 12th International Symposium, FroCoS 2019, London, UK, September 4-6, 2019, Proceedings: 3-21 (2019).
  
• Genetic programming methods for reinforcement learning.
  Robert Babuska
  Proceedings of the Genetic and Evolutionary Computation Conference, GECCO 2019, Prague, Czech Republic, July 13-17, 2019: (2019).
  
• Towards evolutionary theorem proving for isabelle/HOL.
  Yutaka Nagashima
  Proceedings of the Genetic and Evolutionary Computation Conference Companion, GECCO 2019, Prague, Czech Republic, July 13-17, 2019.: 419-420 (2019).
  
• Plant Layout Optimization Using Evolutionary Algorithms.
  Jirí Kubalík, Petr Kadera, Václav Jirkovský, Lukás Kurilla, Simon Prokop
  Industrial Applications of Holonic and Multi-Agent Systems - 9th International Conference, HoloMAS 2019, Linz, Austria, August 26-29, 2019, Proceedings: 173-188 (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).
  
• Exquisitor at the Lifelog Search Challenge 2019.
  Omar Shahbaz Khan, Björn Þór Jónsson, Jan Zahálka, Stevan Rudinac, Marcel Worring
  Proceedings of the ACM Workshop on Lifelog Search Challenge, LSC@ICMR 2019, Ottawa, ON, Canada, 10 June 2019.: 7-11 (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).
  
• Exquisitor: Breaking the Interaction Barrier for Exploration of 100 Million Images.
  Hanna Ragnarsdóttir, Þórhildur Þorleiksdóttir, Omar Shahbaz Khan, Björn Þór Jónsson, Gylfi Þór Guðmundsson, Jan Zahálka, Stevan Rudinac, Laurent Amsaleg, Marcel Worring
  Proceedings of the 27th ACM International Conference on Multimedia, MM 2019, Nice, France, October 21-25, 2019: 1029-1031 (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).
  
• Evolving Structures in Complex Systems.
  Hugo Cisneros, Josef Sivic, Tomás Mikolov
  IEEE Symposium Series on Computational Intelligence, SSCI 2019, Xiamen, China, December 6-9, 2019: 230-237 (2019).
  
• Superposition Reasoning about Quantified Bitvector Formulas.
  David Damestani, Laura Kovács, Martin Suda
  21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2019, Timisoara, Romania, September 4-7, 2019: 95-99 (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).
  
• TOOLympics 2019: An Overview of Competitions in Formal Methods.
  Ezio Bartocci, Dirk Beyer, Paul E. Black, Grigory Fedyukovich, Hubert Garavel, Arnd Hartmanns, Marieke Huisman, Fabrice Kordon, Julian Nagele, Mihaela Sighireanu, Bernhard Steffen, Martin Suda, Geoff Sutcliffe, Tjark Weber, Akihisa Yamada
  Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III: 3-24 (2019).
  
• Aiming for the Goal with SInE.
  Martin Suda
  Vampire 2018 and Vampire 2019. The 5th and 6th Vampire Workshops: 38-44 (2019).
  
• Place Deduplication with Embeddings.
  Carl Yang, Do Huy Hoang, Tomás Mikolov, Jiawei Han
  The World Wide Web Conference, WWW 2019, San Francisco, CA, USA, May 13-17, 2019: 3420-3426 (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).
  
• Teaching robots to imitate a human with no on-teacher sensors. What are the key challenges?
  Radoslav Skoviera, Karla Stépánová, Michael Tesar, Gabriela Sejnova, Jirí Sedlár, Michal Vavrecka, Robert Babuska, Josef Sivic
  arXiv CoRR abs/1901.08335 (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).
  
• Symbolic Regression Methods for Reinforcement Learning.
  Jirí Kubalík, Jan Zegklitz, Erik Derner, Robert Babuska
  arXiv CoRR abs/1903.09688 (2019).
  
• Symbolic Regression for Constructing Analytic Models in Reinforcement Learning.
  Erik Derner, Jirí Kubalík, Nicola Ancona, Robert Babuska
  arXiv CoRR abs/1903.11483 (2019).
  
• Hammering Mizar by Learning Clause Guidance.
  Jan Jakubuv, Josef Urban
  arXiv CoRR abs/1904.01677 (2019).
  
• Towards Evolutionary Theorem Proving for Isabelle/HOL.
  Yutaka Nagashima
  arXiv CoRR abs/1904.08468 (2019).
  
• Exquisitor: Interactive Learning at Large.
  Björn Þór Jónsson, Omar Shahbaz Khan, Hanna Ragnarsdóttir, Þórhildur Þorleiksdóttir, Jan Zahálka, Stevan Rudinac, Gylfi Þór Guðmundsson, Laurent Amsaleg, Marcel Worring
  arXiv CoRR abs/1904.08689 (2019).
  
• Cantor-Bernstein implies Excluded Middle.
  Cécilia Pradic, Chad E. Brown
  arXiv CoRR abs/1904.09193 (2019).
  
• Identifying collaborators in large codebases.
  Waren Long, Vadim Markovtsev, Hugo Mougard, Egor Bulychev, Jan Hula
  arXiv CoRR abs/1905.06782 (2019).
  
• Guiding Theorem Proving by Recurrent Neural Networks.
  Bartosz Piotrowski, Josef Urban
  arXiv CoRR abs/1905.07961 (2019).
  
• ENIGMAWatch: ProofWatch Meets ENIGMA.
  Zarathustra Amadeus Goertzel, Jan Jakubuv, Josef Urban
  arXiv CoRR abs/1905.09565 (2019).
  
• Towards Finding Longer Proofs.
  Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, Josef Urban
  arXiv CoRR abs/1905.13100 (2019).
  
• LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL.
  Yutaka Nagashima
  arXiv CoRR abs/1906.08084 (2019).
  
• Designing Game of Theorems.
  Yutaka Nagashima
  arXiv CoRR abs/1906.08549 (2019).
  
• Domain-Specific Language to Encode Induction Heuristics.
  Yutaka Nagashima
  arXiv CoRR abs/1907.02594 (2019).
  
• A Tale of Two Set Theories.
  Chad E. Brown, Karol Pak
  arXiv CoRR abs/1907.08368 (2019).
  
• Vision-based Navigation Using Deep Reinforcement Learning.
  Jonás Kulhánek, Erik Derner, Tim de Bruin, Robert Babuska
  arXiv CoRR abs/1908.03627 (2019).
  
• Place Deduplication with Embeddings.
  Carl Yang, Do Huy Hoang, Tomás Mikolov, Jiawei Han
  arXiv CoRR abs/1910.04861 (2019).
  
• Updating Pre-trained Word Vectors and Text Classifiers using Monolingual Alignment.
  Piotr Bojanowski, Onur Celebi, Tomás Mikolov, Edouard Grave, Armand Joulin
  arXiv CoRR abs/1910.06241 (2019).
  
• A scheduling and control approach for an industrial furnace to minimize idle energy consumption.
  Ondrej Benedikt, Baran Alikoc, Premysl Sucha, Sergej Celikovský, Zdenek Hanzálek
  arXiv CoRR abs/1910.07501 (2019).
  
• Deep Reinforcement Learning in HOL4.
  Thibault Gauthier
  arXiv CoRR abs/1910.11797 (2019).
  
• Evolving Structures in Complex Systems.
  Hugo Cisneros, Josef Sivic, Tomás Mikolov
  arXiv CoRR abs/1911.01086 (2019).
  
• Can Neural Networks Learn Symbolic Rewriting?
  Bartosz Piotrowski, Josef Urban, Chad E. Brown, Cezary Kaliszyk
  arXiv CoRR abs/1911.04873 (2019).
  
• Robust cooperative synchronization of homogeneous agents with delays on directed communication graphs.
  Baran Alikoc, Kristian Hengster-Movric
  arXiv CoRR abs/1911.10359 (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).
  
• Proceedings of the Second International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, ARCADE@CADE 2019, Natal, Brazil, August 26, 2019.
  Martin Suda, Sarah Winkler
  EPTCS 311 (2019).
  
• Reinforcement learning based compensation methods for robot manipulators.
  Yudha P. Pane, Subramanya Nageshrao, Jens Kober, Robert Babuska
  Eng. Appl. Artif. Intell. 78: 236-247 (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).
  
• 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).
  
• 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).
  
• SAT Competition 2018.
  Marijn J. H. Heule, Matti Järvisalo, Martin Suda
  J. Satisf. Boolean Model. Comput. 11: 133-154 (2019).
  
• Aligning concepts across proof assistant libraries.
  Thibault Gauthier, Cezary Kaliszyk
  J. Symb. Comput. 90: 89-123 (2019).
  
• An Integrated Approach to Goal Selection in Mobile Robot Exploration.
  Miroslav Kulich, Jirí Kubalík, Libor Preucil
  Sensors 19: (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).
  
• Efficient Large-Scale Multi-Modal Classification.
  Douwe Kiela, Edouard Grave, Armand Joulin, Tomás Mikolov
  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: 5198-5204 (2018).
  
• Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning co-located with Federated Logic Conference 2018 (FLoC 2018), Oxford, UK, July 19th, 2018.
  Boris Konev, Josef Urban, Philipp Rümmer
  CEUR Workshop Proceedings 2162 (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).
  
• Loss in Translation: Learning Bilingual Word Mapping with a Retrieval Criterion.
  Armand Joulin, Piotr Bojanowski, Tomás Mikolov, Hervé Jégou, Edouard Grave
  Proceedings of the 2018 Conference on Empirical Methods in Natural Language Processing, Brussels, Belgium, October 31 - November 4, 2018: 2979-2984 (2018).
  
• Mathematical Software - ICMS 2018 - 6th International Conference, South Bend, IN, USA, July 24-27, 2018, Proceedings
  James H. Davenport, Manuel Kauers, George Labahn, Josef Urban
  Lecture Notes in Computer Science 10931 (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).
  
• Data-driven Construction of Symbolic Process Models for Reinforcement Learning.
  Erik Derner, Jirí Kubalík, Robert Babuska
  2018 IEEE International Conference on Robotics and Automation, ICRA 2018, Brisbane, Australia, May 21-25, 2018: 1-8 (2018).
  
• Reinforcement Learning with Symbolic Input-Output Models.
  Erik Derner, Jirí Kubalík, Robert Babuska
  2018 IEEE/RSJ International Conference on Intelligent Robots and Systems, IROS 2018, Madrid, Spain, October 1-5, 2018: 3004-3009 (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).
  
• PaMpeR: proof method recommendation system for Isabelle/HOL.
  Yutaka Nagashima, Yilun He
  Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, ASE 2018, Montpellier, France, September 3-7, 2018: 362-372 (2018).
  
• LPAR-22 Workshop and Short Paper Proceedings, Awassa, Ethiopia, 16-21 November 2018
  Gilles Barthe, Konstantin Korovin, Stephan Schulz, Martin Suda, Geoff Sutcliffe, Margus Veanes
  Kalpa Publications in Computing 9 (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).
  
• A Theory of Satisfiability-Preserving Proofs in SAT Solving.
  Adrián Rebola-Pardo, Martin Suda
  LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16-21 November 2018: 583-603 (2018).
  
• Learning Word Vectors for 157 Languages.
  Edouard Grave, Piotr Bojanowski, Prakhar Gupta, Armand Joulin, Tomás Mikolov
  Proceedings of the Eleventh International Conference on Language Resources and Evaluation, LREC 2018, Miyazaki, Japan, May 7-12, 2018.: (2018).
  
• Advances in Pre-Training Distributed Word Representations.
  Tomás Mikolov, Edouard Grave, Piotr Bojanowski, Christian Puhrsch, Armand Joulin
  Proceedings of the Eleventh International Conference on Language Resources and Evaluation, LREC 2018, Miyazaki, Japan, May 7-12, 2018.: (2018).
  
• System Description: XSL-Based Translator of Mizar to LaTeX.
  Grzegorz Bancerek, Adam Naumowicz, Josef Urban
  Intelligent Computer Mathematics - 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings: 1-6 (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).
  
• Goal-Oriented Conjecturing for Isabelle/HOL.
  Yutaka Nagashima, Julian Parsert
  Intelligent Computer Mathematics - 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings: 225-231 (2018).
  
• First Experiments with Neural Translation of Informal to Formal Mathematics.
  Qingxiang Wang, Cezary Kaliszyk, Josef Urban
  Intelligent Computer Mathematics - 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings: 255-270 (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).
  
• Local Soundness for QBF Calculi.
  Martin Suda, Bernhard Gleiss
  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: 217-234 (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).
  
• Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning.
  Giles Reger, Martin Suda, Andrei Voronkov
  Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part I: 3-22 (2018).
  
• Decentralized Reinforcement Learning of Robot Behaviors.
  David Leonardo Leottau, Javier Ruiz-del-Solar, Robert Babuska
  Artif. Intell. 256: 130-159 (2018).
  
• Foreword to the Special Issue on Automated Reasoning.
  Pascal Fontaine, Cezary Kaliszyk, Stephan Schulz, Josef Urban
  AI Commun. 31: 235-236 (2018).
  
• Hierarchical invention of theorem proving strategies.
  Jan Jakubuv, Josef Urban
  AI Commun. 31: 237-250 (2018).
  
• Efficient Large-Scale Multi-Modal Classification.
  Douwe Kiela, Edouard Grave, Armand Joulin, Tomás Mikolov
  arXiv CoRR abs/1802.02892 (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).
  
• Learning Word Vectors for 157 Languages.
  Edouard Grave, Piotr Bojanowski, Prakhar Gupta, Armand Joulin, Tomás Mikolov
  arXiv CoRR abs/1802.06893 (2018).
  
• Learning to Reason with HOL4 tactics.
  Thibault Gauthier, Cezary Kaliszyk, Josef Urban
  arXiv CoRR abs/1804.00595 (2018).
  
• Learning to Prove with Tactics.
  Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, Michael Norrish
  arXiv CoRR abs/1804.00596 (2018).
  
• Improving Supervised Bilingual Mapping of Word Embeddings.
  Armand Joulin, Piotr Bojanowski, Tomás Mikolov, Edouard Grave
  arXiv CoRR abs/1804.07745 (2018).
  
• Machine Learning Guidance and Proof Certification for Connection Tableaux.
  Michael Färber, Cezary Kaliszyk, Josef Urban
  arXiv CoRR abs/1805.03107 (2018).
  
• First Experiments with Neural Translation of Informal to Formal Mathematics.
  Qingxiang Wang, Cezary Kaliszyk, Josef Urban
  arXiv CoRR abs/1805.06502 (2018).
  
• Reinforcement Learning of Theorem Proving.
  Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Mirek Olsák
  arXiv CoRR abs/1805.07563 (2018).
  
• Goal-Oriented Conjecturing for Isabelle/HOL.
  Yutaka Nagashima, Julian Parsert
  arXiv CoRR abs/1806.04774 (2018).
  
• PaMpeR: Proof Method Recommendation System for Isabelle/HOL.
  Yutaka Nagashima, Yilun He
  arXiv CoRR abs/1806.07239 (2018).
  
• Towards Machine Learning Mathematical Induction.
  Yutaka Nagashima
  arXiv CoRR abs/1812.04088 (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).
  
• Policy derivation methods for critic-only reinforcement learning in continuous spaces.
  Eduard Alibekov, Jirí Kubalík, Robert Babuska
  Eng. Appl. Artif. Intell. 69: 178-187 (2018).
  
• Experience Selection in Deep Reinforcement Learning for Control.
  Tim de Bruin, Jens Kober, Karl Tuyls, Robert Babuska
  J. Mach. Learn. Res. 19: 9:1-9:56 (2018).
  
• Integrating State Representation Learning Into Deep Reinforcement Learning.
  Tim de Bruin, Jens Kober, Karl Tuyls, Robert Babuska
  IEEE Robotics Autom. Lett. 3: 1394-1401 (2018).
  
• Model-Plant Mismatch Compensation Using Reinforcement Learning.
  Ivan Koryakovskiy, Manuel Kudruss, Heike Vallery, Robert Babuska, Wouter Caarls
  IEEE Robotics Autom. Lett. 3: 2471-2477 (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).
  
• Blackthorn: Large-Scale Interactive Multimodal Learning.
  Jan Zahálka, Stevan Rudinac, Björn Þór Jónsson, Dennis C. Koelma, Marcel Worring
  IEEE Trans. Multim. 20: 687-698 (2018).
  
• A Multiple-Model Reliability Prediction Approach for Condition-Based Maintenance.
  Kim Verbert, Bart De Schutter, Robert Babuska
  IEEE Trans. Reliab. 67: 1364-1376 (2018).
  
• Reinforcement Learning Applied to an Electric Water Heater: From Theory to Practice.
  Frederik Ruelens, Bert Claessens, Salman Quaiyum, Bart De Schutter, Robert Babuska, Ronnie Belmans
  IEEE Trans. Smart Grid 9: 3792-3800 (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).
  
• Fast Linear Model for Knowledge Graph Embeddings.
  Armand Joulin, Edouard Grave, Piotr Bojanowski, Maximilian Nickel, Tomás Mikolov
  6th Workshop on Automated Knowledge Base Construction, AKBC@NIPS 2017, Long Beach, California, USA, December 8, 2017: (2017).
  
• Detecting Inconsistencies in Large First-Order Knowledge Bases.
  Stephan Schulz, Geoff Sutcliffe, Josef Urban, Adam Pease
  Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings: 310-325 (2017).
  
• Monte Carlo Tableau Proof Search.
  Michael Färber, Cezary Kaliszyk, Josef Urban
  Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings: 563-579 (2017).
  
• Splitting Proofs for Interpolation.
  Bernhard Gleiss, Laura Kovács, Martin Suda
  Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings: 291-309 (2017).
  
• A Unifying Principle for Clause Elimination in First-Order Logic.
  Benjamin Kiesl, Martin Suda
  Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings: 274-290 (2017).
  
• A Proof Strategy Language and Proof Script Generation for Isabelle/HOL.
  Yutaka Nagashima, Ramana Kumar
  Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings: 528-545 (2017).
  
• Checkable Proofs for First-Order Theorem Proving.
  Giles Reger, Martin Suda
  ARCADE 2017, 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, Gothenburg, Sweden, 6th August 2017: 55-63 (2017).
  
• AI at CADE/IJCAR.
  Josef Urban
  ARCADE 2017, 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, Gothenburg, Sweden, 6th August 2017: 33-36 (2017).
  
• Model-based real-time control of a magnetic manipulator system.
  Jan-Willem Damsteeg, Subramanya Nageshrao, Robert Babuska
  56th IEEE Annual Conference on Decision and Control, CDC 2017, Melbourne, Australia, December 12-15, 2017: 3277-3282 (2017).
  
• Formalizing a Fragment of Combinatorics on Words.
  Stepan Holub, Robert Veroff
  Unveiling Dynamics and Complexity - 13th Conference on Computability in Europe, CiE 2017, Turku, Finland, June 12-16, 2017, Proceedings: 24-31 (2017).
  
• Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2016 co-located with the 9th Conference on Intelligent Computer Mathematics (CICM 2016), Bialystok, Poland, July 25-29, 2016.
  Andrea Kohlhase, Paul Libbrecht, Bruce R. Miller, Adam Naumowicz, Walther Neuper, Pedro Quaresma, Frank Wm. Tompa, Martin Suda
  CEUR Workshop Proceedings 1785 (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).
  
• Bag of Tricks for Efficient Text Classification.
  Armand Joulin, Edouard Grave, Piotr Bojanowski, Tomás Mikolov
  Proceedings of the 15th Conference of the European Chapter of the Association for Computational Linguistics, EACL 2017, Valencia, Spain, April 3-7, 2017, Volume 2: Short Papers: 427-431 (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).
  
• CommAI: Evaluating the first steps towards a useful general AI.
  Marco Baroni, Armand Joulin, Allan Jabri, Germán Kruszewski, Angeliki Lazaridou, Klemen Simonic, Tomás Mikolov
  5th International Conference on Learning Representations, ICLR 2017, Toulon, France, April 24-26, 2017, Workshop Track Proceedings: (2017).
  
• Variable Computation in Recurrent Neural Networks.
  Yacine Jernite, Edouard Grave, Armand Joulin, Tomás Mikolov
  5th International Conference on Learning Representations, ICLR 2017, Toulon, France, April 24-26, 2017, Conference Track Proceedings: (2017).
  
• Automated tuning and configuration of path planning algorithms.
  Ruben Burger, Mukunda Bharatheesha, Marc van Bert, Robert Babuska
  2017 IEEE International Conference on Robotics and Automation, ICRA 2017, Singapore, Singapore, May 29 - June 3, 2017: 4371-4376 (2017).
  
• Enhanced Symbolic Regression Through Local Variable Transformations.
  Jirí Kubalík, Erik Derner, Robert Babuska
  Proceedings of the 9th International Joint Conference on Computational Intelligence, IJCCI 2017, Funchal, Madeira, Portugal, November 1-3, 2017.: 91-100 (2017).
  
• Automating Formalization by Statistical and Semantic Parsing of Mathematics.
  Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
  Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings: 12-27 (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).
  
• TacticToe: Learning to Reason with HOL4 Tactics.
  Thibault Gauthier, Cezary Kaliszyk, Josef Urban
  LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017: 125-143 (2017).
  
• Blocked Clauses in First-Order Logic.
  Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits, Armin Biere
  LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017: 31-48 (2017).
  
• Set of Support for Theory Reasoning.
  Giles Reger, Martin Suda
  IWIL@LPAR 2017 Workshop and LPAR-21 Short Presentations, Maun, Botswana, May 7-12, 2017: 124-134 (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).
  
• Classification of Alignments Between Concepts of Formal Mathematical Systems.
  Dennis Müller, Thibault Gauthier, Cezary Kaliszyk, Michael Kohlhase, Florian Rabe
  Intelligent Computer Mathematics - 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings: 83-98 (2017).
  
• Discovering Geographic Regions in the City Using Social Multimedia and Open Data.
  Stevan Rudinac, Jan Zahálka, Marcel Worring
  MultiMedia Modeling - 23rd International Conference, MMM 2017, Reykjavik, Iceland, January 4-6, 2017, Proceedings, Part II: 148-159 (2017).
  
• Instantiation and Pretending to be an SMT Solver with Vampire.
  Giles Reger, Martin Suda, Andrei Voronkov
  Proceedings of the 15th International Workshop on Satisfiability Modulo Theories affiliated with the International Conference on Computer-Aided Verification (CAV 2017), Heidelberg, Germany, July 22 - 23, 2017.: 63-75 (2017).
  
• System Description: Statistical Parsing of Informalized Mizar Formulas.
  Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
  19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2017, Timisoara, Romania, September 21-24, 2017: 169-172 (2017).
  
• Testing a Saturation-Based Theorem Prover: Experiences and Challenges.
  Giles Reger, Martin Suda, Andrei Voronkov
  Tests and Proofs - 11th International Conference, TAP@STAF 2017, Marburg, Germany, July 19-20, 2017, Proceedings: 152-161 (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).
  
• CommAI: Evaluating the first steps towards a useful general AI.
  Marco Baroni, Armand Joulin, Allan Jabri, Germán Kruszewski, Angeliki Lazaridou, Klemen Simonic, Tomás Mikolov
  arXiv CoRR abs/1701.08954 (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).
  
• Blocked Clauses in First-Order Logic.
  Benjamin Kiesl, Martin Suda, Martina Seidl, Hans Tompits, Armin Biere
  arXiv CoRR abs/1702.00847 (2017).
  
• Towards Smart Proof Search for Isabelle.
  Yutaka Nagashima
  arXiv CoRR abs/1701.03037 (2017).
  
• Learning Simpler Language Models with the Delta Recurrent Neural Network Framework.
  II Alexander G. Ororbia, Tomás Mikolov, David Reitter
  arXiv CoRR abs/1703.08864 (2017).
  
• Testing a Saturation-Based Theorem Prover: Experiences and Challenges (Extended Version).
  Giles Reger, Martin Suda, Andrei Voronkov
  arXiv CoRR abs/1704.03391 (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).
  
• Fast Linear Model for Knowledge Graph Embeddings.
  Armand Joulin, Edouard Grave, Piotr Bojanowski, Maximilian Nickel, Tomás Mikolov
  arXiv CoRR abs/1710.10881 (2017).
  
• Splitting Proofs for Interpolation.
  Bernhard Gleiss, Laura Kovács, Martin Suda
  arXiv CoRR abs/1711.02503 (2017).
  
• Advances in Pre-Training Distributed Word Representations.
  Tomás Mikolov, Edouard Grave, Piotr Bojanowski, Christian Puhrsch, Armand Joulin
  arXiv CoRR abs/1712.09405 (2017).
  
• Combining knowledge and historical data for system-level fault diagnosis of HVAC systems.
  Kim Verbert, Robert Babuska, Bart De Schutter
  Eng. Appl. Artif. Intell. 59: 260-273 (2017).
  
• Bayesian and Dempster-Shafer reasoning for knowledge-based fault diagnosis-A comparative study.
  Kim Verbert, Robert Babuska, Bart De Schutter
  Eng. Appl. Artif. Intell. 60: 136-150 (2017).
  
• Learning Simpler Language Models with the Differential State Framework.
  II Alexander G. Ororbia, Tomás Mikolov, David Reitter
  Neural Comput. 29: (2017).
  
• Benchmarking model-free and model-based optimal control.
  Ivan Koryakovskiy, Manuel Kudruss, Robert Babuska, Wouter Caarls, Christian Kirches, Katja D. Mombaur, Johannes P. Schlöder, Heike Vallery
  Robotics Auton. Syst. 92: 81-90 (2017).
  
• Timely condition-based maintenance planning for multi-component systems.
  Kim Verbert, Bart De Schutter, Robert Babuska
  Reliab. Eng. Syst. Saf. 159: 310-321 (2017).
  
• A Polynomial Method for Stability Analysis of LTI Systems Independent of Delays.
  Baran Alikoc, Ali Fuat Ergenç
  SIAM J. Control. Optim. 55: 2661-2683 (2017).
  
• Enriching Word Vectors with Subword Information.
  Piotr Bojanowski, Edouard Grave, Armand Joulin, Tomás Mikolov
  Trans. Assoc. Comput. Linguistics 5: 135-146 (2017).
  
• Railway Track Circuit Fault Diagnosis Using Recurrent Neural Networks.
  Tim de Bruin, Kim Verbert, Robert Babuska
  IEEE Trans. Neural Networks Learn. Syst. 28: 523-533 (2017).
  
• Residential Demand Response of Thermostatically Controlled Loads Using Batch Reinforcement Learning.
  Frederik Ruelens, Bert J. Claessens, Stijn Vandael, Bart De Schutter, Robert Babuska, Ronnie Belmans
  IEEE Trans. Smart Grid 8: 2149-2159 (2017).
  
• Stability analysis of multiple time-delay systems and design of time-delay filters (Çoklu zaman gecikmeli sistemlerin kararlılık analizi ve gecikme tabanlı filtre tasarımı)
  Baran Alikoc
  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).
  
• CoGENT: Verifying High-Assurance File System Implementations.
  Sidney Amani, Alex Hixon, Zilin Chen, Christine Rizkallah, Peter Chubb, Liam O'Connor, Joel Beeren, Yutaka Nagashima, Japheth Lim, Thomas Sewell, Joseph Tuong, Gabriele Keller, Toby C. Murray, Gerwin Klein, Gernot Heiser
  Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2016, Atlanta, GA, USA, April 2-6, 2016: 175-188 (2016).
  
• Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning co-located with International Joint Conference on Automated Reasoning (IJCAR 2016), Coimbra, Portugal, July 2nd, 2016.
  Pascal Fontaine, Stephan Schulz, Josef Urban
  CEUR Workshop Proceedings 1635 (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).
  
• Selecting the Selection.
  Krystof Hoder, Giles Reger, Martin Suda, Andrei Voronkov
  Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings: 313-329 (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).
  
• Global Subsumption Revisited (Briefly).
  Giles Reger, Martin Suda
  Vampire@IJCAR 2016. Proceedings of the 3rd Vampire Workshop, Coimbra, Portugal, July 2, 2016.: 61-73 (2016).
  
• Symbolic method for deriving policy in reinforcement learning.
  Eduard Alibekov, Jirí Kubalík, Robert Babuska
  55th IEEE Conference on Decision and Control, CDC 2016, Las Vegas, NV, USA, December 12-14, 2016: 2789-2795 (2016).
  
• Learning state representation for deep actor-critic control.
  Jelle Munk, Jens Kober, Robert Babuska
  55th IEEE Conference on Decision and Control, CDC 2016, Las Vegas, NV, USA, December 12-14, 2016: 4667-4673 (2016).
  
• Actor-critic reinforcement learning for tracking control in robotics.
  Yudha P. Pane, Subramanya Nageshrao, Robert Babuska
  55th IEEE Conference on Decision and Control, CDC 2016, Las Vegas, NV, USA, December 12-14, 2016: 5819-5826 (2016).
  
• A Roadmap Towards Machine Intelligence.
  Tomás Mikolov, Armand Joulin, Marco Baroni
  Computational Linguistics and Intelligent Text Processing - 17th International Conference, CICLing 2016, Konya, Turkey, April 3-9, 2016, Revised Selected Papers, Part I: 29-61 (2016).
  
• Initial Experiments with Statistical Conjecturing over Large Formal Corpora.
  Thibault Gauthier, Cezary Kaliszyk, Josef Urban
  Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2016 co-located with the 9th Conference on Intelligent Computer Mathematics (CICM 2016), Bialystok, Poland, July 25-29, 2016.: 219-228 (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).
  
• Towards a mizar environment for isabelle: foundations and language.
  Cezary Kaliszyk, Karol Pak, Josef Urban
  Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016: 58-65 (2016).
  
• Integrated dynamic modelling and multivariable control of HVAC components.
  Harish Satyavada, Robert Babuska, Simone Baldi
  15th European Control Conference, ECC 2016, Aalborg, Denmark, June 29 - July 1, 2016: 1171-1176 (2016).
  
• A Clausal Normal Form Translation for FOOL.
  Evgenii Kotelnikov, Laura Kovács, Martin Suda, Andrei Voronkov
  GCAI 2016. 2nd Global Conference on Artificial Intelligence, September 19 - October 2, 2016, Berlin, Germany: 53-71 (2016).
  
• New Techniques in Clausal Form Generation.
  Giles Reger, Martin Suda, Andrei Voronkov
  GCAI 2016. 2nd Global Conference on Artificial Intelligence, September 19 - October 2, 2016, Berlin, Germany: 11-23 (2016).
  
• AVATAR Modulo Theories.
  Giles Reger, Nikolaj S. Bjørner, Martin Suda, Andrei Voronkov
  GCAI 2016. 2nd Global Conference on Artificial Intelligence, September 19 - October 2, 2016, Berlin, Germany: 39-52 (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).
  
• Refinement through restraint: bringing down the cost of verification.
  Liam O'Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth Lim, Toby C. Murray, Yutaka Nagashima, Thomas Sewell, Gerwin Klein
  Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016: 89-102 (2016).
  
• Learning Simple Algorithms from Examples.
  Wojciech Zaremba, Tomás Mikolov, Armand Joulin, Rob Fergus
  Proceedings of the 33nd International Conference on Machine Learning, ICML 2016, New York City, NY, USA, June 19-24, 2016: 421-429 (2016).
  
• Deep convolutional neural networks for detection of rail surface defects.
  Shahrzad Faghih-Roohi, Siamak Hajizadeh, Alfredo Núñez, Robert Babuska, Bart De Schutter
  2016 International Joint Conference on Neural Networks, IJCNN 2016, Vancouver, BC, Canada, July 24-29, 2016: 2584-2589 (2016).
  
• Improved deep reinforcement learning for robotics through distribution-based experience retention.
  Tim de Bruin, Jens Kober, Karl Tuyls, Robert Babuska
  2016 IEEE/RSJ International Conference on Intelligent Robots and Systems, IROS 2016, Daejeon, South Korea, October 9-14, 2016: 3947-3952 (2016).
  
• Learning Intelligent Theorem Proving from Large Formal Corpora.
  Josef Urban
  International Symposium on Artificial Intelligence and Mathematics, ISAIM 2016, Fort Lauderdale, Florida, USA, January 4-6, 2016.: (2016).
  
• A Framework for the Automatic Formal Verification of Refinement from Cogent to C.
  Christine Rizkallah, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Zilin Chen, Liam O'Connor, Toby C. Murray, Gabriele Keller, Gerwin Klein
  Interactive Theorem Proving - 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings: 323-340 (2016).
  
• Interactive Multimodal Learning on 100 Million Images.
  Jan Zahálka, Stevan Rudinac, Björn Þór Jónsson, Dennis C. Koelma, Marcel Worring
  Proceedings of the 2016 ACM on International Conference on Multimedia Retrieval, ICMR 2016, New York, New York, USA, June 6-9, 2016: 333-337 (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).
  
• Ten Research Questions for Scalable Multimedia Analytics.
  Björn Þór Jónsson, Marcel Worring, Jan Zahálka, Stevan Rudinac, Laurent Amsaleg
  MultiMedia Modeling - 22nd International Conference, MMM 2016, Miami, FL, USA, January 4-6, 2016, Proceedings, Part II: 290-302 (2016).
  
• DeepMath - Deep Sequence Models for Premise Selection.
  Geoffrey Irving, Christian Szegedy, Alexander A. Alemi, Niklas Eén, François Chollet, Josef Urban
  Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Processing Systems 2016, December 5-10, 2016, Barcelona, Spain: 2235-2243 (2016).
  
• Decentralized Reinforcement Learning Applied to Mobile Robots.
  David Leonardo Leottau, Aashish Vatsyayan, Javier Ruiz-del-Solar, Robert Babuska
  RoboCup 2016: Robot World Cup XX [Leipzig, Germany, June 30 - July 4, 2016]: 368-379 (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).
  
• Finding Finite Models in Multi-sorted First-Order Logic.
  Giles Reger, Martin Suda, Andrei Voronkov
  Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings: 323-341 (2016).
  
• Nested compliant admittance control for robotic mechanical assembly of misaligned and tightly toleranced parts.
  Nicky Mol, Jan Smisek, Robert Babuska, Andre Schiele
  2016 IEEE International Conference on Systems, Man, and Cybernetics, SMC 2016, Budapest, Hungary, October 9-12, 2016: 2717-2722 (2016).
  
• Proof Strategy Language.
  Yutaka Nagashima
  Arch. Formal Proofs 2016: (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).
  
• The CADE-25 Automated Theorem Proving system competition - CASC-25.
  Geoff Sutcliffe, Josef Urban
  AI Commun. 29: 423-433 (2016).
  
• Optimal model-free output synchronization of heterogeneous systems using off-policy reinforcement learning.
  Hamidreza Modares, Subramanya Nageshrao, Gabriel Alexandre Delgado Lopes, Robert Babuska, Frank L. Lewis
  Autom. 71: 334-341 (2016).
  
• Quantified maximum satisfiability.
  Alexey Ignatiev, Mikolás Janota, João Marques-Silva
  Constraints An Int. J. 21: 277-302 (2016).
  
• DeepMath - Deep Sequence Models for Premise Selection.
  Alexander A. Alemi, François Chollet, Geoffrey Irving, Christian Szegedy, Josef Urban
  arXiv CoRR abs/1606.04442 (2016).
  
• Lifting QBF Resolution Calculi to DQBF.
  Olaf Beyersdorff, Leroy Chew, Renate A. Schmidt, Martin Suda
  arXiv CoRR abs/1604.08058 (2016).
  
• Enriching Word Vectors with Subword Information.
  Piotr Bojanowski, Edouard Grave, Armand Joulin, Tomás Mikolov
  arXiv CoRR abs/1607.04606 (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).
  
• Monte Carlo Connection Prover.
  Michael Färber, Cezary Kaliszyk, Josef Urban
  arXiv CoRR abs/1611.05990 (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).
  
• Variable Computation in Recurrent Neural Networks.
  Yacine Jernite, Edouard Grave, Armand Joulin, Tomás Mikolov
  arXiv CoRR abs/1611.06188 (2016).
  
• FastText.zip: Compressing text classification models.
  Armand Joulin, Edouard Grave, Piotr Bojanowski, Matthijs Douze, Hervé Jégou, Tomás Mikolov
  arXiv CoRR abs/1612.03651 (2016).
  
• Bag of Tricks for Efficient Text Classification.
  Armand Joulin, Edouard Grave, Piotr Bojanowski, Tomás Mikolov
  arXiv CoRR abs/1607.01759 (2016).
  
• Semantic Parsing of Mathematics by Context-based Learning from Aligned Corpora and Theorem Proving.
  Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
  arXiv CoRR abs/1611.09703 (2016).
  
• A Proof Strategy Language and Proof Script Generation for Isabelle.
  Yutaka Nagashima, Ramana Kumar
  arXiv CoRR abs/1606.02941 (2016).
  
• Close Encounters of the Higher Kind Emulating Constructor Classes in Standard ML.
  Yutaka Nagashima, Liam O'Connor
  arXiv CoRR abs/1608.03350 (2016).
  
• COGENT: Certified Compilation for a Functional Systems Language.
  Liam O'Connor, Christine Rizkallah, Zilin Chen, Sidney Amani, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Alex Hixon, Gabriele Keller, Toby C. Murray, Gerwin Klein
  arXiv CoRR abs/1601.05520 (2016).
  
• Finding Finite Models in Multi-Sorted First Order Logic.
  Giles Reger, Martin Suda, Andrei Voronkov
  arXiv CoRR abs/1604.08040 (2016).
  
• Selecting the Selection.
  Giles Reger, Martin Suda, Andrei Voronkov, Krystof Hoder
  arXiv CoRR abs/1604.08055 (2016).
  
• Towards AI-Complete Question Answering: A Set of Prerequisite Toy Tasks.
  Jason Weston, Antoine Bordes, Sumit Chopra, Tomás Mikolov
  4th International Conference on Learning Representations, ICLR 2016, San Juan, Puerto Rico, May 2-4, 2016, Conference Track Proceedings: (2016).
  
• Synchronization of a class of cyclic discrete-event systems describing legged locomotion.
  Gabriel A. D. Lopes, Bart Kersbergen, Bart De Schutter, Ton J. J. van den Boom, Robert Babuska
  Discret. Event Dyn. Syst. 26: 225-261 (2016).
  
• Online learning for optimistic planning.
  Lucian Busoniu, Alexander Daniels, Robert Babuska
  Eng. Appl. Artif. Intell. 55: 70-82 (2016).
  
• Fault diagnosis using spatial and temporal information with application to railway track circuits.
  Kim Verbert, Bart De Schutter, Robert Babuska
  Eng. Appl. Artif. Intell. 56: 200-211 (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).
  
• A Learning-Based Fact Selector for Isabelle/HOL.
  Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, Josef Urban
  J. Autom. Reason. 57: 219-244 (2016).
  
• Hammering towards QED.
  Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, Josef Urban
  J. Formaliz. Reason. 9: 101-148 (2016).
  
• Preface: Twenty Years of the QED Manifesto.
  John Harrison, Josef Urban, Freek Wiedijk
  J. Formaliz. Reason. 9: 1-2 (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).
  
• Port-Hamiltonian Systems in Adaptive and Learning Control: A Survey.
  Subramanya Nageshrao, Gabriel A. D. Lopes, Dimitri Jeltsema, Robert Babuska
  IEEE Trans. Autom. Control. 61: 1223-1238 (2016).
  
• Hybrid Single Node Genetic Programming for Symbolic Regression.
  Jirí Kubalík, Eduard Alibekov, Jan Zegklitz, Robert Babuska
  Trans. Comput. Collect. Intell. 24: 61-82 (2016).
  
• Learning Sequential Composition Control.
  Esmaeil Najafi, Robert Babuska, Gabriel A. D. Lopes
  IEEE Trans. Cybern. 46: 2559-2569 (2016).
  
• Multimedia Pivot Tables for Multimedia Analytics on Image Collections.
  Marcel Worring, Dennis C. Koelma, Jan Zahálka
  IEEE Trans. Multim. 18: 2217-2227 (2016).
  
• Unified Modeling and Control of Walking and Running on the Spring-Loaded Inverted Pendulum.
  Mohammad Shahbazi, Robert Babuska, Gabriel A. D. Lopes
  IEEE Trans. Robotics 32: 1178-1195 (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).
  
• System Description: E.T. 0.1.
  Cezary Kaliszyk, Stephan Schulz, Josef Urban, Jirí Vyskocil
  Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings: 389-398 (2015).
  
• The Uses of SAT Solvers in Vampire.
  Giles Reger, Martin Suda
  Proceedings of the 1st and 2nd Vampire Workshops, Vampire@VSL 2014, Vienna, Austria, July 23, 2014 / Vampire@CADE 2015, Berlin, Germany, August 2, 2015: 63-69 (2015).
  
• Playing with AVATAR.
  Giles Reger, Martin Suda, Andrei Voronkov
  Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings: 399-415 (2015).
  
• Premise Selection and External Provers for HOL4.
  Thibault Gauthier, Cezary Kaliszyk
  Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015: 49-57 (2015).
  
• Certified Connection Tableaux Proofs for HOL Light and TPTP.
  Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
  Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015: 59-66 (2015).
  
• Real-Time Optimistic Planning with Action Sequences.
  Thijs Wensveen, Lucian Busoniu, Robert Babuska
  20th International Conference on Control Systems and Computer Science, CSCS 2015, Bucharest, Romania, May 27-29, 2015: 923-930 (2015).
  
• Exploiting spatial and temporal dependencies to enhance fault diagnosis: Application to railway track circuits.
  Kim Verbert, Bart De Schutter, Robert Babuska
  14th European Control Conference, ECC 2015, Linz, Austria, July 15-17, 2015: 3047-3052 (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).
  
• Lemmatization for Stronger Reasoning in Large Theories.
  Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
  Frontiers of Combining Systems - 10th International Symposium, FroCoS 2015, Wroclaw, Poland, September 21-24, 2015. Proceedings: 341-356 (2015).
  
• BliStr: The Blind Strategymaker.
  Josef Urban
  Global Conference on Artificial Intelligence, GCAI 2015, Tbilisi, Georgia, October 16-19, 2015: 312-319 (2015).
  
• Selection Hyper-Heuristic Using a Portfolio of Derivative Heuristics.
  Frantisek Hruska, Jirí Kubalík
  Genetic and Evolutionary Computation Conference, GECCO 2015, Madrid, Spain, July 11-15, 2015, Companion Material Proceedings: 1401-1402 (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).
  
• Analytical approximation for the double-stance phase of a walking robot.
  Mohammad Shahbazi, Robert Babuska, Gabriel A. D. Lopes
  IEEE International Conference on Robotics and Automation, ICRA 2015, Seattle, WA, USA, 26-30 May, 2015: 5754-5760 (2015).
  
• Attitude and altitude estimation and control on board a Flapping Wing Micro Air Vehicle.
  J. L. Verboom, Sjoerd Tijmons, Christophe De Wagter, B. D. W. Remes, Robert Babuska, Guido C. H. E. de Croon
  IEEE International Conference on Robotics and Automation, ICRA 2015, Seattle, WA, USA, 26-30 May, 2015: 5846-5851 (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 Semantic Features for Automated Reasoning over Large Theories.
  Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
  Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015: 3084-3090 (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).
  
• An Improved Single Node Genetic Programming for Symbolic Regression.
  Jirí Kubalík, Robert Babuska
  Proceedings of the 7th International Joint Conference on Computational Intelligence (IJCCI 2015) - Volume 1: ECTA, Lisbon, Portugal, November 12-14, 2015.: 244-251 (2015).
  
• Learning to Parse on Aligned Corpora (Rough Diamond).
  Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
  Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings: 227-233 (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).
  
• Sharing HOL4 and HOL Light Proof Knowledge.
  Thibault Gauthier, Cezary Kaliszyk
  Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings: 372-386 (2015).
  
• FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover.
  Cezary Kaliszyk, Josef Urban
  Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings: 88-96 (2015).
  
• Improving Statistical Linguistic Algorithms for Parsing Mathematics.
  Cezary Kaliszyk, Josef Urban, Jirí Vyskocil
  IWIL@LPAR 2015, 11th International Workshop on the Implementation of Logics, Suva, Fiji, November 23, 2015: 27-36 (2015).
  
• Experiments with State-of-the-art Automated Provers on Problems in Tarskian Geometry.
  Josef Urban, Robert Veroff
  IWIL@LPAR 2015, 11th International Workshop on the Implementation of Logics, Suva, Fiji, November 23, 2015: 122-126 (2015).
  
• Level control of a coupled-tank system via eigenvalue assignment and LQG control.
  Deniz Engules, Murat Hot, Baran Alikoc
  23rd Mediterranean Conference on Control and Automation, MED 2015, Torremolinos, Malaga, Spain, June 16-19, 2015: 1198-1203 (2015).
  
• Mizar: State-of-the-art and Beyond.
  Grzegorz Bancerek, Czeslaw Bylinski, Adam Grabowski, Artur Kornilowicz, Roman Matuszewski, Adam Naumowicz, Karol Pak, Josef Urban
  Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings: 261-279 (2015).
  
• Auto-hyperlinking the Stacks Project.
  Johan Commelin, Josef Urban
  informal CICM 2015 - Informal Work in Progress Proceedings, Washington, DC, USA, July 13-17, 2015 (2015).
  
• Formalizing Physics: Automation, Presentation and Foundation Issues.
  Cezary Kaliszyk, Josef Urban, Umair Siddique, Sanaz Khan Afshar, Cvetan Dunchev, Sofiène Tahar
  Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings: 288-295 (2015).
  
• Analytic Quality: Evaluation of Performance and Insight in Multimedia Collection Analysis.
  Jan Zahálka, Stevan Rudinac, Marcel Worring
  Proceedings of the 23rd Annual ACM Conference on Multimedia Conference, MM '15, Brisbane, Australia, October 26 - 30, 2015: 231-240 (2015).
  
• Inferring Algorithmic Patterns with Stack-Augmented Recurrent Nets.
  Armand Joulin, Tomás Mikolov
  Advances in Neural Information Processing Systems 28: Annual Conference on Neural Information Processing Systems 2015, December 7-12, 2015, Montreal, Quebec, Canada: 190-198 (2015).
  
• An application of sequential composition control to cooperative systems.
  Esmaeil Najafi, Robert Babuska, Gabriel A. D. Lopes
  10th International Workshop on Robot Motion and Control, RoMoCo 2015, Poznań, Poland, July 6-8, 2015: 15-20 (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).
  
• Alternative structures for character-level RNNs.
  Piotr Bojanowski, Armand Joulin, Tomás Mikolov
  arXiv CoRR abs/1511.06303 (2015).
  
• Sharing HOL4 and HOL Light proof knowledge.
  Thibault Gauthier, Cezary Kaliszyk
  arXiv CoRR abs/1509.03527 (2015).
  
• Premise Selection and External Provers for HOL4.
  Thibault Gauthier, Cezary Kaliszyk
  arXiv CoRR abs/1509.03534 (2015).
  
• A formal proof of the Kepler conjecture.
  Thomas C. Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason M. Rute, Alexey Solovyev, An Hoai Thi Ta, Trung Nam Tran, Diep Thi Trieu, Josef Urban, Ky Khac Vu, Roland Zumkeller
  arXiv CoRR abs/1501.02155 (2015).
  
• Inferring Algorithmic Patterns with Stack-Augmented Recurrent Nets.
  Armand Joulin, Tomás Mikolov
  arXiv CoRR abs/1503.01007 (2015).
  
• Ensemble of Generative and Discriminative Techniques for Sentiment Analysis of Movie Reviews.
  Grégoire Mesnil, Tomás Mikolov, Marc'Aurelio Ranzato, Yoshua Bengio
  3rd International Conference on Learning Representations, ICLR 2015, San Diego, CA, USA, May 7-9, 2015, Workshop Track Proceedings: (2015).
  
• A Roadmap towards Machine Intelligence.
  Tomás Mikolov, Armand Joulin, Marco Baroni
  arXiv CoRR abs/1511.08130 (2015).
  
• Learning Longer Memory in Recurrent Neural Networks.
  Tomás Mikolov, Armand Joulin, Sumit Chopra, Michaël Mathieu, Marc'Aurelio Ranzato
  3rd International Conference on Learning Representations, ICLR 2015, San Diego, CA, USA, May 7-9, 2015, Workshop Track Proceedings: (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).
  
• Reinforcement Learning Applied to an Electric Water Heater: From Theory to Practice.
  Frederik Ruelens, Bert Claessens, Salman Quaiyum, Bart De Schutter, Robert Babuska, Ronnie Belmans
  arXiv CoRR abs/1512.00408 (2015).
  
• Residential Demand Response Applications Using Batch Reinforcement Learning.
  Frederik Ruelens, Bert Claessens, Stijn Vandael, Bart De Schutter, Robert Babuska, Ronnie Belmans
  arXiv CoRR abs/1504.02125 (2015).
  
• Learning Simple Algorithms from Examples.
  Wojciech Zaremba, Tomás Mikolov, Armand Joulin, Rob Fergus
  arXiv CoRR abs/1511.07275 (2015).
  
• Reconsidering Pairs and Functions as Sets.
  Chad E. Brown
  J. Autom. Reason. 55: 199-210 (2015).
  
• Erratum to : Learning-Assisted Automated Reasoning with Flyspeck.
  Cezary Kaliszyk, Josef Urban
  J. Autom. Reason. 54: (2015).
  
• MizAR 40 for Mizar 40.
  Cezary Kaliszyk, Josef Urban
  J. Autom. Reason. 55: 245-256 (2015).
  
• MaLeS: A Framework for Automatic Tuning of Automated Theorem Provers.
  Daniel Kühlwein, Josef Urban
  J. Autom. Reason. 55: 91-116 (2015).
  
• Learning-assisted theorem proving with millions of lemmas.
  Cezary Kaliszyk, Josef Urban
  J. Symb. Comput. 69: 109-128 (2015).
  
• Undecidability of Consequence Relation in Full non-Associative Lambek Calculus.
  Karel Chvalovský
  J. Symb. Log. 80: 567-586 (2015).
  
• HOL(y)Hammer: Online ATP Service for HOL Light.
  Cezary Kaliszyk, Josef Urban
  Math. Comput. Sci. 9: 5-22 (2015).
  
• Variable and Clause Elimination for LTL Satisfiability Checking.
  Martin Suda
  Math. Comput. Sci. 9: 327-344 (2015).
  
• Learning robustly stable open-loop motions for robotic manipulation.
  Wouter Wolfslag, Michiel Plooij, Robert Babuska, Martijn Wisse
  Robotics Auton. Syst. 66: 27-34 (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).
  
• Reinforcement Learning for Port-Hamiltonian Systems.
  Olivier Sprangers, Robert Babuska, Subramanya Nageshrao, Gabriel A. D. Lopes
  IEEE Trans. Cybern. 45: 1003-1013 (2015).
  
• Interactive Multimodal Learning for Venue Recommendation.
  Jan Zahálka, Stevan Rudinac, Marcel Worring
  IEEE Trans. Multim. 17: 2235-2244 (2015).
  
• Resolution-based methods for linear temporal reasoning.
  Martin Suda
  Thesis (2015).