Activities

Competitions

Meetings

Visitors

Publications

    2020

  1. Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, Josef Urban.
    Exploration of neural machine translation in autoformalization of mathematics in Mizar.
    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).
  2. Jan Jakubuv, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, Josef Urban.
    ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description).
    arXiv CoRR abs/2002.05406 (2020).
  3. Lasse Blaauwbroek, Josef Urban, Herman Geuvers.
    Tactic Learning and Proving for the Coq Proof Assistant.
    arXiv CoRR abs/2003.09140 (2020).
  4. Bernhard Gleiss, Martin Suda.
    Layered Clause Selection for Theory Reasoning.
    arXiv CoRR abs/2001.09705 (2020).
  5. Yutaka Nagashima.
    Smart Induction for Isabelle/HOL (System Description).
    arXiv CoRR abs/2001.10834 (2020).
  6. 2019

  7. Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban.
    GRUNGE: A Grand Unified ATP Challenge.
    Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings: 123-141 (2019).
  8. Karel Chvalovský, Jan Jakubuv, Martin Suda, Josef Urban.
    ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E.
    Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings: 197-215 (2019).
  9. Jan Jakubuv, Josef Urban.
    Hammering Mizar by Learning Clause Guidance (Short Paper).
    10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA.: 34:1-34:8 (2019).
  10. Zarathustra Goertzel, Jan Jakubuv, Josef Urban.
    ENIGMAWatch: ProofWatch Meets ENIGMA.
    Automated Reasoning with Analytic Tableaux and Related Methods - 28th International Conference, TABLEAUX 2019, London, UK, September 3-5, 2019, Proceedings: 374-388 (2019).
  11. Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban.
    GRUNGE: A Grand Unified ATP Challenge.
    arXiv CoRR abs/1903.02539 (2019).
  12. Karel Chvalovský, Jan Jakubuv, Martin Suda, Josef Urban.
    ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E.
    arXiv CoRR abs/1903.03182 (2019).
  13. Jan Jakubuv, Josef Urban.
    Hammering Mizar by Learning Clause Guidance.
    arXiv CoRR abs/1904.01677 (2019).
  14. Bartosz Piotrowski, Josef Urban.
    Guiding Theorem Proving by Recurrent Neural Networks.
    arXiv CoRR abs/1905.07961 (2019).
  15. Zarathustra Goertzel, Jan Jakubuv, Josef Urban.
    ENIGMAWatch: ProofWatch Meets ENIGMA.
    arXiv CoRR abs/1905.09565 (2019).
  16. Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, Josef Urban.
    Towards Finding Longer Proofs.
    arXiv CoRR abs/1905.13100 (2019).
  17. Bartosz Piotrowski, Josef Urban, Chad E. Brown, Cezary Kaliszyk.
    Can Neural Networks Learn Symbolic Rewriting?
    arXiv CoRR abs/1911.04873 (2019).
  18. Miroslav Olsák, Cezary Kaliszyk, Josef Urban.
    Property Invariant Embedding for Automated Reasoning.
    arXiv CoRR abs/1911.12073 (2019).
  19. Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, Josef Urban.
    Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar.
    arXiv CoRR abs/1912.02636 (2019).
  20. Karel Chvalovský.
    Top-Down Neural Model For Formulae.
    7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019: (2019).
  21. Olaf Beyersdorff, Joshua Blinkhorn, Leroy Chew, Renate A. Schmidt, Martin Suda.
    Reinterpreting Dependency Schemes: Soundness Meets Incompleteness in DQBF.
    J. Autom. Reasoning 63: 597-623 (2019).
  22. Giles Reger, Martin Riener, Martin Suda.
    Symmetry Avoidance in MACE-Style Finite Model Finding.
    Frontiers of Combining Systems - 12th International Symposium, FroCoS 2019, London, UK, September 4-6, 2019, Proceedings: 3-21 (2019).
  23. 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.
    TOOLympics 2019: An Overview of Competitions in Formal Methods.
    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).
  24. Chad E. Brown, Cezary Kaliszyk, Karol Pak.
    Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
    10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA.: 9:1-9:16 (2019).
  25. Chad E. Brown, Karol Pak.
    A Tale of Two Set Theories.
    Intelligent Computer Mathematics - 12th International Conference, CICM 2019, Prague, Czech Republic, July 8-12, 2019, Proceedings: 44-60 (2019).
  26. Pierre Pradic, Chad E. Brown.
    Cantor-Bernstein implies Excluded Middle.
    arXiv CoRR abs/1904.09193 (2019).
  27. Chad E. Brown, Karol Pak.
    A Tale of Two Set Theories.
    arXiv CoRR abs/1907.08368 (2019).
  28. Chad E. Brown, Thibault Gauthier.
    Self-Learned Formula Synthesis in Set Theory.
    arXiv CoRR abs/1912.01525 (2019).
  29. Thibault Gauthier, Cezary Kaliszyk.
    Aligning concepts across proof assistant libraries.
    J. Symb. Comput. 90: 89-123 (2019).
  30. Thibault Gauthier.
    Deep Reinforcement Learning in HOL4.
    arXiv CoRR abs/1910.11797 (2019).
  31. Yutaka Nagashima.
    LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL.
    Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings: 266-287 (2019).
  32. Yutaka Nagashima.
    Towards evolutionary theorem proving for isabelle/HOL.
    Proceedings of the Genetic and Evolutionary Computation Conference Companion, GECCO 2019, Prague, Czech Republic, July 13-17, 2019.: 419-420 (2019).
  33. Yutaka Nagashima.
    Towards Evolutionary Theorem Proving for Isabelle/HOL.
    arXiv CoRR abs/1904.08468 (2019).
  34. Yutaka Nagashima.
    LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL.
    arXiv CoRR abs/1906.08084 (2019).
  35. Yutaka Nagashima.
    Designing Game of Theorems.
    arXiv CoRR abs/1906.08549 (2019).
  36. Yutaka Nagashima.
    Domain-Specific Language to Encode Induction Heuristics.
    arXiv CoRR abs/1907.02594 (2019).
  37. Olaf Beyersdorff, Leroy Chew, Mikolás Janota.
    New Resolution-Based QBF Calculi and Their Proof Complexity.
    TOCT 11: 26:1-26:42 (2019).
  38. Mikolás Janota.
    On Unordered BDDs and Quantified Boolean Formulas.
    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).
  39. Mikolás Janota, Inês Lynce.
    Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings
    Lecture Notes in Computer Science 11628 (2019).
  40. Simon Cooksey, Sarah Harris, Mark Batty, Radu Grigore, Mikolás Janota.
    PrideMM: A Solver for Relaxed Memory Models.
    arXiv CoRR abs/1901.00428 (2019).
  41. 2018

  42. Pascal Fontaine, Cezary Kaliszyk, Stephan Schulz, Josef Urban.
    Foreword to the Special Issue on Automated Reasoning.
    AI Commun. 31: 235-236 (2018).
  43. Jan Jakubuv, Josef Urban.
    Hierarchical invention of theorem proving strategies.
    AI Commun. 31: 237-250 (2018).
  44. Bartosz Piotrowski, Josef Urban.
    ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback.
    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).
  45. Zarathustra Goertzel, Jan Jakubuv, Stephan Schulz, Josef Urban.
    ProofWatch: Watchlist Guidance for Large Theories in E.
    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).
  46. Grzegorz Bancerek, Adam Naumowicz, Josef Urban.
    System Description: XSL-Based Translator of Mizar to LaTeX.
    Intelligent Computer Mathematics - 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings: 1-6 (2018).
  47. Jan Jakubuv, Josef Urban.
    Enhancing ENIGMA Given Clause Guidance.
    Intelligent Computer Mathematics - 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings: 118-124 (2018).
  48. Qingxiang Wang, Cezary Kaliszyk, Josef Urban.
    First Experiments with Neural Translation of Informal to Formal Mathematics.
    Intelligent Computer Mathematics - 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings: 255-270 (2018).
  49. Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Miroslav Olsák.
    Reinforcement Learning of Theorem Proving.
    Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, 3-8 December 2018, Montréal, Canada.: 8836-8847 (2018).
  50. Boris Konev, Josef Urban, Philipp Rümmer.
    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.
    CEUR Workshop Proceedings 2162 (2018).
  51. James H. Davenport, Manuel Kauers, George Labahn, Josef Urban.
    Mathematical Software - ICMS 2018 - 6th International Conference, South Bend, IN, USA, July 24-27, 2018, Proceedings
    Lecture Notes in Computer Science 10931 (2018).
  52. Bartosz Piotrowski, Josef Urban.
    ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback.
    arXiv CoRR abs/1802.03375 (2018).
  53. Zarathustra Goertzel, Jan Jakubuv, Stephan Schulz, Josef Urban.
    ProofWatch: Watchlist Guidance for Large Theories in E.
    arXiv CoRR abs/1802.04007 (2018).
  54. Thibault Gauthier, Cezary Kaliszyk, Josef Urban.
    Learning to Reason with HOL4 tactics.
    arXiv CoRR abs/1804.00595 (2018).
  55. Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, Michael Norrish.
    Learning to Prove with Tactics.
    arXiv CoRR abs/1804.00596 (2018).
  56. Michael Färber, Cezary Kaliszyk, Josef Urban.
    Machine Learning Guidance and Proof Certification for Connection Tableaux.
    arXiv CoRR abs/1805.03107 (2018).
  57. Qingxiang Wang, Cezary Kaliszyk, Josef Urban.
    First Experiments with Neural Translation of Informal to Formal Mathematics.
    arXiv CoRR abs/1805.06502 (2018).
  58. Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Mirek Olsák.
    Reinforcement Learning of Theorem Proving.
    arXiv CoRR abs/1805.07563 (2018).
  59. Jan Jakubuv, Cezary Kaliszyk.
    Towards a Unified Ordering for Superposition-Based Automated Reasoning.
    Mathematical Software - ICMS 2018 - 6th International Conference, South Bend, IN, USA, July 24-27, 2018, Proceedings: 245-254 (2018).
  60. Mikolas Janota, Martin Suda.
    Towards Smarter MACE-style Model Finders.
    LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16-21 November 2018: 454-470 (2018).
  61. Adrián Rebola-Pardo, Martin Suda.
    A Theory of Satisfiability-Preserving Proofs in SAT Solving.
    LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16-21 November 2018: 583-603 (2018).
  62. Yutaka Nagashima, Yilun He.
    PaMpeR: proof method recommendation system for Isabelle/HOL.
    Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, ASE 2018, Montpellier, France, September 3-7, 2018: 362-372 (2018).
  63. Yutaka Nagashima, Julian Parsert.
    Goal-Oriented Conjecturing for Isabelle/HOL.
    Intelligent Computer Mathematics - 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings: 225-231 (2018).
  64. Yutaka Nagashima, Julian Parsert.
    Goal-Oriented Conjecturing for Isabelle/HOL.
    arXiv CoRR abs/1806.04774 (2018).
  65. Yutaka Nagashima, Yilun He.
    PaMpeR: Proof Method Recommendation System for Isabelle/HOL.
    arXiv CoRR abs/1806.07239 (2018).
  66. Yutaka Nagashima.
    Towards Machine Learning Mathematical Induction.
    arXiv CoRR abs/1812.04088 (2018).
  67. Mikolás Janota.
    Towards Generalization in QBF Solving via Machine Learning.
    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).
  68. Mikolás Janota.
    Circuit-Based Search Space Pruning in QBF.
    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).
  69. 2017

  70. Stephan Schulz, Geoff Sutcliffe, Josef Urban, Adam Pease.
    Detecting Inconsistencies in Large First-Order Knowledge Bases.
    Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings: 310-325 (2017).
  71. Michael Färber, Cezary Kaliszyk, Josef Urban.
    Monte Carlo Tableau Proof Search.
    Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings: 563-579 (2017).
  72. Thibault Gauthier, Cezary Kaliszyk, Josef Urban.
    TacticToe: Learning to Reason with HOL4 Tactics.
    LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017: 125-143 (2017).
  73. Jan Jakubuv, Martin Suda, Josef Urban.
    Automated Invention of Strategies and Term Orderings for Vampire.
    GCAI 2017, 3rd Global Conference on Artificial Intelligence, Miami, FL, USA, 18-22 October 2017.: 121-133 (2017).
  74. Jan Jakubuv, Josef Urban.
    ENIGMA: Efficient Learning-Based Inference Guiding Machine.
    Intelligent Computer Mathematics - 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings: 292-302 (2017).
  75. Jan Jakubuv, Josef Urban.
    BliStrTune: hierarchical invention of theorem proving strategies.
    Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017: 43-52 (2017).
  76. Cezary Kaliszyk, Josef Urban, Jirí Vyskocil.
    Automating Formalization by Statistical and Semantic Parsing of Mathematics.
    Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings: 12-27 (2017).
  77. Josef Urban.
    AI at CADE/IJCAR.
    ARCADE 2017, 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, Gothenburg, Sweden, 6th August 2017: 33-36 (2017).
  78. 2016

  79. Cezary Kaliszyk, Josef Urban, Jirí Vyskocil.
    Semantic Parsing of Mathematics by Context-based Learning from Aligned Corpora and Theorem Proving.
    arXiv CoRR abs/1611.09703 (2016).
  80. Michael Färber, Chad E. Brown.
    Internal Guidance for Satallax.
    arXiv CoRR abs/1605.09293 (2016).
  81. Jan Jakubuv, Josef Urban.
    BliStrTune: Hierarchical Invention of Theorem Proving Strategies.
    arXiv CoRR abs/1611.08733 (2016).
  82. Michael Färber, Cezary Kaliszyk, Josef Urban.
    Monte Carlo Connection Prover.
    arXiv CoRR abs/1611.05990 (2016).
  83. Alex A. Alemi, François Chollet, Geoffrey Irving, Christian Szegedy, Josef Urban.
    DeepMath - Deep Sequence Models for Premise Selection.
    arXiv CoRR abs/1606.04442 (2016).
  84. Jan Jakubuv, Josef Urban.
    Extending E Prover with Similarity Based Clause Selection Strategies.
    arXiv CoRR abs/1606.03888 (2016).
  85. Chad E. Brown, Josef Urban.
    Extracting Higher-Order Goals from the Mizar Mathematical Library.
    arXiv CoRR abs/1605.06996 (2016).
  86. Pascal Fontaine, Stephan Schulz, Josef Urban.
    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.
    CEUR Workshop Proceedings 1635 (2016).
  87. Jan Jakubuv, Josef Urban.
    Extending E Prover with Similarity Based Clause Selection Strategies.
    Intelligent Computer Mathematics - 9th International Conference, CICM 2016, Bialystok, Poland, July 25-29, 2016, Proceedings: 151-156 (2016).
  88. Michael Färber, Chad E. Brown.
    Internal Guidance for Satallax.
    Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings: 349-361 (2016).
  89. Chad E. Brown, Josef Urban.
    Extracting Higher-Order Goals from the Mizar Mathematical Library.
    Intelligent Computer Mathematics - 9th International Conference, CICM 2016, Bialystok, Poland, July 25-29, 2016, Proceedings: 99-114 (2016).
  90. Cezary Kaliszyk, Karol Pak, Josef Urban.
    Towards a mizar environment for isabelle: foundations and language.
    Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016: 58-65 (2016).
  91. Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, Josef Urban.
    Hammering towards QED.
    J. Formalized Reasoning 9(1): 101-148 (2016).
  92. John Harrison, Josef Urban, Freek Wiedijk.
    Preface: Twenty Years of the QED Manifesto.
    J. Formalized Reasoning 9(1): 1-2 (2016).
  93. Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, Josef Urban.
    A Learning-Based Fact Selector for Isabelle/HOL.
    J. Autom. Reasoning 57(3): 219-244 (2016).
  94. Cezary Kaliszyk, Josef Urban.
    Wikis and Collaborative Systems for Large Formal Mathematics.
    Semantic Web Collaborative Spaces - Second International Workshop, SWCS 2013, Montpellier, France, May 27, 2013, Third International Workshop, SWCS 2014, Trentino, Italy, October 19, 2014, Revised Selected and Invited Papers: 35-52 (2016).
  95. 2015

  96. Cezary Kaliszyk, Josef Urban, Jiri Vyskocil.
    Improving Statistical Linguistic Algorithms for Parsing Mathematics.
    EPiC Series in Computing, 11th International Workshop on the Implementation of Logics, Proceedings: 27-36 (2015).
  97. Josef Urban, Robert Veroff.
    Experiments with State-of-the-art Automated Provers on Problems in Tarskian Geometry.
    EPiC Series in Computing, 11th International Workshop on the Implementation of Logics, Proceedings: 122-126 (2015).
  98. Cezary Kaliszyk, Josef Urban.
    FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover.
    Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings: 88-96 (2015).
  99. Josef Urban.
    BliStr: The Blind Strategymaker.
    Global Conference on Artificial Intelligence, GCAI 2015, Tbilisi, Georgia, October 16-19, 2015: 312-319 (2015).
  100. Cezary Kaliszyk, Josef Urban, Jirí Vyskocil.
    Lemmatization for Stronger Reasoning in Large Theories.
    Frontiers of Combining Systems - 10th International Symposium, FroCoS 2015, Wroclaw, Poland, September 21-24, 2015. Proceedings: 341-356 (2015).