Activities

Publications

2024

• Beneficial AGI: Care and Collaboration Are All You Need.
  Zarathustra Amadeus Goertzel
  Artificial General Intelligence - 17th International Conference, AGI 2024, Seattle, WA, USA, August 13-16, 2024, Proceedings: 84-88 (2024).
  
• Learning Guided Automated Reasoning: A Brief Survey.
  Lasse Blaauwbroek, David M. Cerna, Thibault Gauthier, Jan Jakubuv, Cezary Kaliszyk, Martin Suda, Josef Urban
  Logics and Type Systems in Theory and Practice - Essays Dedicated to Herman Geuvers on The Occasion of His 60th Birthday: 54-83 (2024).
  
• Graph2Tac: Online Representation Learning of Formal Math Concepts.
  Lasse Blaauwbroek, Mirek Olsák, Jason Rute, Fidel Ivan Schaposnik Massolo, Jelle Piepenbrock, Vasily Pestun
  Forty-first International Conference on Machine Learning, ICML 2024, Vienna, Austria, July 21-27, 2024: (2024).
  
• Regularization in Spider-Style Strategy Discovery and Schedule Construction.
  Filip Bártek, Karel Chvalovský, Martin Suda
  Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I: 194-213 (2024).
  
• A Higher-Order Vampire (Short Paper).
  Ahmed Bhayat, Martin Suda
  Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I: 75-85 (2024).
  
• Lemma Discovery and Strategies for Automated Induction.
  Sólrún Halla Einarsdóttir, Márton Hajdú, Moa Johansson, Nicholas Smallbone, Martin Suda
  Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I: 214-232 (2024).
  
• A Formal Proof of R(4, 5)=25.
  Thibault Gauthier, Chad E. Brown
  15th International Conference on Interactive Theorem Proving, ITP 2024, September 9-14, 2024, Tbilisi, Georgia: 16:1-16:18 (2024).
  
• Prover9 Unleashed: Automated Configuration for Enhanced Proof Discovery.
  Kristina Aleksandrova, Jan Jakubuv, Cezary Kaliszyk
  LPAR 2024: Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning, Port Louis, Mauritius, May 26-31, 2024: 360-369 (2024).
  
• First Experiments with Neural cvc5.
  Jelle Piepenbrock, Mikolas Janota, Josef Urban, Jan Jakubuv
  LPAR 2024: Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning, Port Louis, Mauritius, May 26-31, 2024: 264-277 (2024).
  
• Solving Hard Mizar Problems with Instantiation and Strategy Invention.
  Jan Jakubuv, Mikolás Janota, Josef Urban
  Intelligent Computer Mathematics - 17th International Conference, CICM 2024, Montréal, QC, Canada, August 5-9, 2024, Proceedings: 315-333 (2024).
  
• Joint Proceedings of the 9th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 9th Satisfiability Checking and Symbolic Computation Workshop (SC-Square), 2024 co-located with the 12th International Joint Conference on Automated Reasoning (IJCAR 2024), Nancy, France, July 2, 2024.
  Christopher W. Brown, Daniela Kaufmann, Cláudia Nalon, Alexander Steen, Martin Suda
  CEUR Workshop Proceedings 3717 (2024).
  
• Cautious Specialization of Strategy Schedules (Extended Abstract).
  Filip Bártek, Karel Chvalovský, Martin Suda
  Joint Proceedings of the 9th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 9th Satisfiability Checking and Symbolic Computation Workshop (SC-Square), 2024 co-located with the 12th International Joint Conference on Automated Reasoning (IJCAR 2024), Nancy, France, July 2, 2024.: 28-36 (2024).
  
• 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).
  
• Learning Guided Automated Reasoning: A Brief Survey.
  Lasse Blaauwbroek, David M. Cerna, Thibault Gauthier, Jan Jakubuv, Cezary Kaliszyk, Martin Suda, Josef Urban
  arXiv CoRR abs/2403.04017 (2024).
  
• Regularization in Spider-Style Strategy Discovery and Schedule Construction.
  Filip Bártek, Karel Chvalovský, Martin Suda
  arXiv CoRR abs/2403.12869 (2024).
  
• A Formal Proof of R(4, 5)=25.
  Thibault Gauthier, Chad E. Brown
  arXiv CoRR abs/2404.01761 (2024).
  
• Solving Hard Mizar Problems with Instantiation and Strategy Invention.
  Jan Jakubuv, Mikolás Janota, Josef Urban
  arXiv CoRR abs/2406.17762 (2024).
  
• A Higher-Order Vampire (Short Paper).
  Ahmed Bhayat, Martin Suda
  arXiv CoRR abs/2407.05208 (2024).
  
• Hashing Modulo Context-Sensitive 𝛼-Equivalence.
  Lasse Blaauwbroek, Miroslav Olsák, Herman Geuvers
  Proc. ACM Program. Lang. 8: 2027-2050 (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).
  
• 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).
  
• 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).
  
• VizAR: Visualization of Automated Reasoning Proofs (System Description).
  Jan Jakubuv, Cezary Kaliszyk
  Intelligent Computer Mathematics - 16th International Conference, CICM 2023, Cambridge, UK, September 5-8, 2023, Proceedings: 303-308 (2023).
  
• Selecting Quantifiers for Instantiation in SMT.
  Jan Jakubuv, Mikolás Janota, Bartosz Piotrowski, Jelle Piepenbrock, Andrew Reynolds
  Proceedings of the 21st International Workshop on Satisfiability Modulo Theories (SMT 2023) co-located with the 29th International Conference on Automated Deduction (CADE 2023), Rome, Italy, July, 5-6, 2023.: 71-77 (2023).
  
• Towards Learning Infinite SMT Models (Work in Progress).
  Mikolás Janota, Bartosz Piotrowski, Karel Chvalovský
  25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2023, Nancy, France, September 11-14, 2023: 82-85 (2023).
  
• 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).
  
• Alien Coding.
  Thibault Gauthier, Miroslav Olsák, Josef Urban
  arXiv CoRR abs/2301.11479 (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).
  
• A Mathematical Benchmark for Inductive Theorem Provers.
  Thibault Gauthier, Chad E. Brown, Mikolas Janota, Josef Urban
  arXiv CoRR abs/2304.02986 (2023).
  
• Translating SUMO-K to Higher-Order Set Theory.
  Chad E. Brown, Adam Pease, Josef Urban
  arXiv CoRR abs/2305.07903 (2023).
  
• An Evaluation of GPT-4 on the ETHICS Dataset.
  Sergey Rodionov, Zarathustra Amadeus Goertzel, Ben Goertzel
  arXiv CoRR abs/2309.10492 (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).
  
• Alien coding.
  Thibault Gauthier, Miroslav Olsák, Josef Urban
  Int. J. Approx. Reason. 162: (2023/11).
  

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).
  
• 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).
  
• 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).
  
• 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).
  
• 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).
  
• 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).
  
• A Wos Challenge Met.
  Robert Veroff
  J. Autom. Reason. 66: 565-574 (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).
  
• 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).
  
• 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).
  
• 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).
  
• 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).
  
• SAT Competition 2020.
  Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda
  Artif. Intell. 301: (2021).
  
• Vampire With a Brain Is a Good ITP Hammer.
  Martin Suda
  arXiv CoRR abs/2102.03529 (2021).
  
• Learning Equational Theorem Proving.
  Jelle Piepenbrock, Tom Heskes, Mikolás Janota, Josef Urban
  arXiv CoRR abs/2102.05547 (2021).
  
• New Techniques that Improve ENIGMA-style Clause Selection Guidance.
  Martin Suda
  arXiv CoRR abs/2102.13564 (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).
  
• 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).
  
• 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).
  
• 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).
  

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).
  
• 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).
  
• 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).
  
• 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).
  
• 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).
  
• 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).
  
• Tactic Learning and Proving for the Coq Proof Assistant.
  Lasse Blaauwbroek, Josef Urban, Herman Geuvers
  arXiv CoRR abs/2003.09140 (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).
  
• Towards United Reasoning for Automatic Induction in Isabelle/HOL.
  Yutaka Nagashima
  arXiv CoRR abs/2005.12737 (2020).
  
• First Neural Conjecturing Datasets and Experiments.
  Josef Urban, Jan Jakubuv
  arXiv CoRR abs/2005.14664 (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).
  
• 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).
  
• SeLFiE: Modular Semantic Reasoning for Induction in Isabelle/HOL.
  Yutaka Nagashima
  arXiv CoRR abs/2010.10296 (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).
  

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).
  
• 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).
  
• 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).
  
• 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).
  
• 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).
  
• 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).
  
• GRUNGE: A Grand Unified ATP Challenge.
  Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban
  arXiv CoRR abs/1903.02539 (2019).
  
• ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E.
  Karel Chvalovský, Jan Jakubuv, Martin Suda, Josef Urban
  arXiv CoRR abs/1903.03182 (2019).
  
• Hammering Mizar by Learning Clause Guidance.
  Jan Jakubuv, Josef Urban
  arXiv CoRR abs/1904.01677 (2019).
  
• Towards Evolutionary Theorem Proving for Isabelle/HOL.
  Yutaka Nagashima
  arXiv CoRR abs/1904.08468 (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).
  
• Deep Reinforcement Learning in HOL4.
  Thibault Gauthier
  arXiv CoRR abs/1910.11797 (2019).
  
• Can Neural Networks Learn Symbolic Rewriting?
  Bartosz Piotrowski, Josef Urban, Chad E. Brown, Cezary Kaliszyk
  arXiv CoRR abs/1911.04873 (2019).
  
• Property Invariant Embedding for Automated Reasoning.
  Miroslav Olsák, Cezary Kaliszyk, Josef Urban
  arXiv CoRR abs/1911.12073 (2019).
  
• Self-Learned Formula Synthesis in Set Theory.
  Chad E. Brown, Thibault Gauthier
  arXiv CoRR abs/1912.01525 (2019).
  
• Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar.
  Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, Josef Urban
  arXiv CoRR abs/1912.02636 (2019).
  
• 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).
  
• 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).
  
• 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).
  

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).
  
• 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).
  
• 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).
  
• 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).
  
• 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).
  
• 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).
  
• 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 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).
  
• 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).
  
• Recursive Reductions of Action Dependencies for Coordination-Based Multiagent Planning.
  Jan Tozicka, Jan Jakubuv, Antonín Komenda
  Trans. Comput. Collect. Intell. 28: 66-92 (2018).
  

2017

• 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).
  
• 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).
  
• 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).
  
• 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).
  
• 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).
  
• 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).
  
• ENIGMA: Efficient Learning-based Inference Guiding Machine.
  Jan Jakubuv, Josef Urban
  arXiv CoRR abs/1701.06532 (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).
  
• Testing a Saturation-Based Theorem Prover: Experiences and Challenges (Extended Version).
  Giles Reger, Martin Suda, Andrei Voronkov
  arXiv CoRR abs/1704.03391 (2017).
  
• Splitting Proofs for Interpolation.
  Bernhard Gleiss, Laura Kovács, Martin Suda
  arXiv CoRR abs/1711.02503 (2017).
  

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).
  
• 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).
  
• 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).
  
• 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).
  
• 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).
  
• 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 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).
  
• 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).
  
• 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).
  
• 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).
  
• 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).
  
• Proof Strategy Language.
  Yutaka Nagashima
  Arch. Formal Proofs 2016: (2016).
  
• The CADE-25 Automated Theorem Proving system competition - CASC-25.
  Geoff Sutcliffe, Josef Urban
  AI Commun. 29: 423-433 (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).
  
• Extracting Higher-Order Goals from the Mizar Mathematical Library.
  Chad E. Brown, Josef Urban
  arXiv CoRR abs/1605.06996 (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).
  
• 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).
  
• Lifting QBF Resolution Calculi to DQBF.
  Olaf Beyersdorff, Leroy Chew, Renate A. Schmidt, Martin Suda
  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).
  
• Full Lambek Calculus with Contraction is Undecidable.
  Karel Chvalovský, Rostislav Horcík
  J. Symb. Log. 81: 524-540 (2016).
  
• Privacy-concerned multiagent planning.
  Jan Tozicka, Jan Jakubuv, Antonín Komenda, Michal Pechoucek
  Knowl. Inf. Syst. 48: 581-618 (2016).
  

2015

• 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).
  
• 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).
  
• 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).
  
• 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).
  
• 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).
  
• 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).
  
• 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).
  
• 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).
  
• 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).
  
• 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).
  
• Resolution-based methods for linear temporal reasoning.
  Martin Suda
  Thesis (2015).