Activities

Competitions

• 2018: CASC J9
  • Satallax 3.3 won in category Higher-order Theorems (THF).
  • MaLARea 0.6 won in category Large Theory Batch Problems (LTB).
• 2017: CASC 26
  • Satallax 3.2 won in category Higher-order Theorems (THF).
• 2016: CASC J8
  • Satallax 3.0 won in category Higher-order Theorems (THF).
  • We co-developed the AIM, CML, and HLL problems in Large Theory Batch Problems (LTB).

Meetings

• CICM'19 Conference
• AITP'19 Conference
• AITP'18 Conference
• BUMERANG'18 Workshop
• VINO'17 Workshop
• ARG Seminars
• ARG Workshops
• AITP'17 Conference
• VORACE'17 Workshop
• AITP'16 Conference

Visitors

• Miroslav Olšák (2020)
• Constantin Ruhdorfer (2020)
• Jelle Piepenbrock (2019)
• Bob Veroff (2019)
• Zsolt Zombori (2019)
• John Hester (2019)
• Deepak Kapur (2019)
• Yuli Daune Funato (2019)
• Robert Veroff (16.4. - 19.6.2018)
• Michael Beeson (2017)
• Ramana Kumar (2017)
• Geoff Sutcliffe (2017)
• Robert Veroff (3.4. - 31.5.2017)
• Ondřej Kunčar (27.4. - 30.4.2017)
• John Harrison (19.3. - 22.3.2017)
• Thibault Gauthier (30.1 - 4.3.2017)
• Karol Pak (22.11. - 26.11.2016)
• Jens Otten (26.9. - 28.9. 2016)
• Christian Szegedy (21.9. - 28.9.2016)
• Jasmin Blanchette (21.9. - 23.9.2016)
• Stephan Schulz (21.9 - 25.9.2016)
• Ondřej Kunčar (21.9. - 25.9.2016)
• Martin Suda (21.9. - 25.9.2016)
• Thibault Gauthier (7.9 - 28.9.2016)
• Michael Faerber (1.7. - 1.11.2016)
• Robert Veroff (8.4. - 31.5.2016)
• Thibault Gauthier (2.3. - 23.3.2016)
• Jens Otten (7.11. - 11.11.2015)
• Cezary Kaliszyk (7.11. - 10.11.2015)
• Stephan Schulz (7.11. - 10.11.2015)
• Karol Pak (7.11. - 10.11.2015)
• Lukasz Czajka (6.11. - 10.11.2015)
• Michael Faerber (1.11. - 20.11.2015)

Publications

2021

1. Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds.
   Fair and Adventurous Enumeration of Quantifier Instantiations.
   Formal Methods in Computer Aided Design, FMCAD 2021, New Haven, CT, USA, October 19-22, 2021: 256-260 (2021).
   [ BibTeX | doi | dblp ]
2. Zsolt Zombori, Josef Urban, Miroslav Olsák.
   The Role of Entropy in Guiding a Connection Prover.
   arXiv CoRR abs/2105.14706 (2021).
   [ BibTeX | arXiv | dblp ]
3. Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban.
   Learning Theorem Proving Components.
   arXiv CoRR abs/2107.10034 (2021).
   [ BibTeX | arXiv | dblp ]
4. Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda.
   SAT Competition 2020.
   Artif. Intell. 301: (2021).
   [ BibTeX | doi | dblp ]
5. Martin Suda.
   Vampire With a Brain Is a Good ITP Hammer.
   arXiv CoRR abs/2102.03529 (2021).
   [ BibTeX | arXiv | dblp ]
6. Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds.
   Fair and Adventurous Enumeration of Quantifier Instantiations.
   arXiv CoRR abs/2105.13700 (2021).
   [ BibTeX | arXiv | dblp ]
7. Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, Michael Norrish.
   TacticToe: Learning to Prove with Tactics.
   J. Autom. Reason. 65: 257-286 (2021).
   [ BibTeX | doi | dblp ]
8. Chad Brown, Mikolás Janota.
   First-Order Instantiation using Discriminating Terms.
   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).
   [ BibTeX | url | dblp ]
9. Jan Jakubuv, Mikolás Janota, Andrew Reynolds.
   Characteristic Subsets of SMT-LIB Benchmarks.
   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).
   [ BibTeX | url | dblp ]
10. Zarathustra Amadeus Goertzel, Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban.
    Fast and Slow Enigmas and Parental Guidance.
    arXiv CoRR abs/2107.06750 (2021).
    [ BibTeX | arXiv | dblp ]
11. Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban.
    Learning Theorem Proving Components.
    Automated Reasoning with Analytic Tableaux and Related Methods - 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6-9, 2021, Proceedings: 266-278 (2021).
    [ BibTeX | doi | dblp ]
12. Filip Bártek, Martin Suda.
    Neural Precedence Recommender.
    Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings: 525-542 (2021).
    [ BibTeX | doi | dblp ]
13. Zarathustra Amadeus Goertzel, Karel Chvalovský, Jan Jakubuv, Miroslav Olsák, Josef Urban.
    Fast and Slow Enigmas and Parental Guidance.
    Frontiers of Combining Systems - 13th International Symposium, FroCoS 2021, Birmingham, UK, September 8-10, 2021, Proceedings: 173-191 (2021).
    [ BibTeX | doi | dblp ]
14. Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Prokop Cerný, Cezary Kaliszyk, Josef Urban.
    Online Machine Learning Techniques for Coq: A Comparison.
    Intelligent Computer Mathematics - 14th International Conference, CICM 2021, Timisoara, Romania, July 26-31, 2021, Proceedings: 67-83 (2021).
    [ BibTeX | doi | dblp ]
15. Martin Suda.
    Vampire with a Brain Is a Good ITP Hammer.
    Frontiers of Combining Systems - 13th International Symposium, FroCoS 2021, Birmingham, UK, September 8-10, 2021, Proceedings: 192-209 (2021).
    [ BibTeX | doi | dblp ]
16. Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Prokop Cerný, Cezary Kaliszyk, Josef Urban.
    Online Machine Learning Techniques for Coq: A Comparison.
    arXiv CoRR abs/2104.05207 (2021).
    [ BibTeX | arXiv | dblp ]
17. Jaroslav Macke, Jirí Sedlár, Miroslav Olsák, Josef Urban, Josef Sivic.
    Learning to Solve Geometric Construction Problems from Images.
    Intelligent Computer Mathematics - 14th International Conference, CICM 2021, Timisoara, Romania, July 26-31, 2021, Proceedings: 167-184 (2021).
    [ BibTeX | doi | dblp ]
18. Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, Josef Urban.
    Towards Finding Longer Proofs.
    Automated Reasoning with Analytic Tableaux and Related Methods - 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6-9, 2021, Proceedings: 167-186 (2021).
    [ BibTeX | doi | dblp ]
19. Jan Hula, David Mojzísek, Mikolás Janota.
    Graph Neural Networks for Scheduling of SMT Solvers.
    33rd IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2021, Washington, DC, USA, November 1-3, 2021: 447-451 (2021).
    [ BibTeX | doi | dblp ]
20. Martin Suda.
    New Techniques that Improve ENIGMA-style Clause Selection Guidance.
    arXiv CoRR abs/2102.13564 (2021).
    [ BibTeX | arXiv | dblp ]
21. Yutaka Nagashima.
    Faster Smarter Proof by Induction in Isabelle/HOL.
    Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event / Montreal, Canada, 19-27 August 2021.: 1981-1988 (2021).
    [ BibTeX | doi | dblp ]
22. Jaroslav Macke, Jirí Sedlár, Miroslav Olsák, Josef Urban, Josef Sivic.
    Learning to solve geometric construction problems from images.
    arXiv CoRR abs/2106.14195 (2021).
    [ BibTeX | arXiv | dblp ]
23. Thibault Gauthier.
    Learned Provability Likelihood for Tactical Search.
    Proceedings of the 9th International Symposium on Symbolic Computation in Software Science, SCSS 2021, Hagenberg, Austria, September 8-10, 2021.: 78-85 (2021).
    [ BibTeX | arXiv | dblp ]
24. Mikolás Janota, António Morgado, José Fragoso Santos, Vasco M. Manquinho.
    The Seesaw Algorithm: Function Optimization Using Implicit Hitting Sets.
    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).
    [ BibTeX | doi | dblp ]
25. Zsolt Zombori, Josef Urban, Miroslav Olsák.
    The Role of Entropy in Guiding a Connection Prover.
    Automated Reasoning with Analytic Tableaux and Related Methods - 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6-9, 2021, Proceedings: 218-235 (2021).
    [ BibTeX | doi | dblp ]
26. João Araújo, Choiwah Chow, Mikolás Janota.
    Filtering Isomorphic Models by Invariants (Short Paper).
    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).
    [ BibTeX | doi | dblp ]
27. Michael Färber, Cezary Kaliszyk, Josef Urban.
    Machine Learning Guidance for Connection Tableaux.
    J. Autom. Reason. 65: 287-320 (2021).
    [ BibTeX | doi | dblp ]
28. Martin Suda.
    Improving ENIGMA-style Clause Selection while Learning From History.
    Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings: 543-561 (2021).
    [ BibTeX | doi | dblp ]
29. Jelle Piepenbrock, Tom Heskes, Mikolás Janota, Josef Urban.
    Learning Equational Theorem Proving.
    arXiv CoRR abs/2102.05547 (2021).
    [ BibTeX | arXiv | dblp ]

2020

30. Bernhard Gleiss, Martin Suda.
    Layered Clause Selection for Theory Reasoning.
    arXiv CoRR abs/2001.09705 (2020).
    [ BibTeX | arXiv | dblp ]
31. Josef Urban, Jan Jakubuv.
    First Neural Conjecturing Datasets and Experiments.
    Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings: 315-323 (2020).
    [ BibTeX | doi | dblp ]
32. George Labahn, James H. Davenport, Josef Urban.
    Foreword.
    Math. Comput. Sci. 14: 531-532 (2020).
    [ BibTeX | doi | dblp ]
33. Jan Jakubuv, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, Josef Urban.
    ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description).
    Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II: 448-463 (2020).
    [ BibTeX | doi | dblp ]
34. Bartosz Piotrowski, Josef Urban.
    Stateful Premise Selection by Recurrent Neural Networks.
    LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020.: 409-422 (2020).
    [ BibTeX | easychair | dblp ]
35. Yutaka Nagashima.
    Towards United Reasoning for Automatic Induction in Isabelle/HOL.
    arXiv CoRR abs/2005.12737 (2020).
    [ BibTeX | arXiv | dblp ]
36. Thibault Gauthier.
    Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic.
    LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020.: 230-248 (2020).
    [ BibTeX | easychair | dblp ]
37. Jan Jakubuv, Cezary Kaliszyk.
    Relaxed Weighted Path Order in Theorem Proving.
    Math. Comput. Sci. 14: 657-670 (2020).
    [ BibTeX | doi | dblp ]
38. Yutaka Nagashima.
    Simple Dataset for Proof Method Recommendation in Isabelle/HOL.
    Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings: 297-302 (2020).
    [ BibTeX | doi | dblp ]
39. Lasse Blaauwbroek, Josef Urban, Herman Geuvers.
    Tactic Learning and Proving for the Coq Proof Assistant.
    arXiv CoRR abs/2003.09140 (2020).
    [ BibTeX | arXiv | dblp ]
40. Lasse Blaauwbroek, Josef Urban, Herman Geuvers.
    Tactic Learning and Proving for the Coq Proof Assistant.
    LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020.: 138-150 (2020).
    [ BibTeX | easychair | dblp ]
41. Yutaka Nagashima.
    Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description).
    arXiv CoRR abs/2004.10667 (2020).
    [ BibTeX | arXiv | dblp ]
42. 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).
    [ BibTeX | doi | dblp ]
43. Zsolt Zombori, Josef Urban, Chad E. Brown.
    Prolog Technology Reinforcement Learning Prover.
    arXiv CoRR abs/2004.06997 (2020).
    [ BibTeX | arXiv | dblp ]
44. Lasse Blaauwbroek, Josef Urban, Herman Geuvers.
    The Tactician - A Seamless, Interactive Tactic Learner and Prover for Coq.
    Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings: 271-277 (2020).
    [ BibTeX | doi | dblp ]
45. Bernhard Gleiss, Martin Suda.
    Layered Clause Selection for Theory Reasoning - (Short Paper).
    Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part I: 402-409 (2020).
    [ BibTeX | doi | dblp ]
46. Josef Urban, Jan Jakubuv.
    First Neural Conjecturing Datasets and Experiments.
    arXiv CoRR abs/2005.14664 (2020).
    [ BibTeX | arXiv | dblp ]
47. Mikolás Janota, António Morgado.
    SAT-Based Encodings for Optimal Decision Trees with Explicit Paths.
    Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings: 501-518 (2020).
    [ BibTeX | doi | dblp ]
48. Bartosz Piotrowski, Josef Urban.
    Stateful Premise Selection by Recurrent Neural Networks.
    arXiv CoRR abs/2004.08212 (2020).
    [ BibTeX | arXiv | dblp ]
49. Thibault Gauthier.
    Tree Neural Networks in HOL4.
    Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings: 278-283 (2020).
    [ BibTeX | doi | dblp ]
50. Lasse Blaauwbroek, Josef Urban, Herman Geuvers.
    The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq.
    arXiv CoRR abs/2008.00120 (2020).
    [ BibTeX | arXiv | dblp ]
51. 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).
    [ BibTeX | arXiv | dblp ]
52. Zsolt Zombori, Josef Urban, Chad E. Brown.
    Prolog Technology Reinforcement Learning Prover - (System Description).
    Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II: 489-507 (2020).
    [ BibTeX | doi | dblp ]
53. Yutaka Nagashima.
    Smart Induction for Isabelle/HOL (System Description).
    arXiv CoRR abs/2001.10834 (2020).
    [ BibTeX | arXiv | dblp ]
54. Bartosz Piotrowski, Josef Urban.
    Guiding Inferences in Connection Tableau by Recurrent Neural Networks.
    Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings: 309-314 (2020).
    [ BibTeX | doi | dblp ]

2019

55. 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).
    [ BibTeX | doi | dblp ]
56. 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).
    [ BibTeX | doi | dblp ]
57. 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).
    [ BibTeX | doi | dblp ]
58. 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).
    [ BibTeX | doi | dblp ]
59. Chad E. Brown, Thibault Gauthier, Cezary Kaliszyk, Geoff Sutcliffe, Josef Urban.
    GRUNGE: A Grand Unified ATP Challenge.
    arXiv CoRR abs/1903.02539 (2019).
    [ BibTeX | arXiv | dblp ]
60. 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).
    [ BibTeX | arXiv | dblp ]
61. Jan Jakubuv, Josef Urban.
    Hammering Mizar by Learning Clause Guidance.
    arXiv CoRR abs/1904.01677 (2019).
    [ BibTeX | arXiv | dblp ]
62. Bartosz Piotrowski, Josef Urban.
    Guiding Theorem Proving by Recurrent Neural Networks.
    arXiv CoRR abs/1905.07961 (2019).
    [ BibTeX | arXiv | dblp ]
63. Zarathustra Goertzel, Jan Jakubuv, Josef Urban.
    ENIGMAWatch: ProofWatch Meets ENIGMA.
    arXiv CoRR abs/1905.09565 (2019).
    [ BibTeX | arXiv | dblp ]
64. Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, Josef Urban.
    Towards Finding Longer Proofs.
    arXiv CoRR abs/1905.13100 (2019).
    [ BibTeX | arXiv | dblp ]
65. Bartosz Piotrowski, Josef Urban, Chad E. Brown, Cezary Kaliszyk.
    Can Neural Networks Learn Symbolic Rewriting?
    arXiv CoRR abs/1911.04873 (2019).
    [ BibTeX | arXiv | dblp ]
66. Miroslav Olsák, Cezary Kaliszyk, Josef Urban.
    Property Invariant Embedding for Automated Reasoning.
    arXiv CoRR abs/1911.12073 (2019).
    [ BibTeX | arXiv | dblp ]
67. 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).
    [ BibTeX | arXiv | dblp ]
68. 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).
    [ BibTeX | url | dblp ]
69. 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).
    [ BibTeX | url | dblp ]
70. 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).
    [ BibTeX | doi | dblp ]
71. 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).
    [ BibTeX | doi | dblp ]
72. 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).
    [ BibTeX | doi | dblp ]
73. 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).
    [ BibTeX | doi | dblp ]
74. Pierre Pradic, Chad E. Brown.
    Cantor-Bernstein implies Excluded Middle.
    arXiv CoRR abs/1904.09193 (2019).
    [ BibTeX | arXiv | dblp ]
75. Chad E. Brown, Karol Pak.
    A Tale of Two Set Theories.
    arXiv CoRR abs/1907.08368 (2019).
    [ BibTeX | arXiv | dblp ]
76. Chad E. Brown, Thibault Gauthier.
    Self-Learned Formula Synthesis in Set Theory.
    arXiv CoRR abs/1912.01525 (2019).
    [ BibTeX | arXiv | dblp ]
77. Thibault Gauthier, Cezary Kaliszyk.
    Aligning concepts across proof assistant libraries.
    J. Symb. Comput. 90: 89-123 (2019).
    [ BibTeX | doi | dblp ]
78. Thibault Gauthier.
    Deep Reinforcement Learning in HOL4.
    arXiv CoRR abs/1910.11797 (2019).
    [ BibTeX | arXiv | dblp ]
79. 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).
    [ BibTeX | doi | dblp ]
80. 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).
    [ BibTeX | doi | dblp ]
81. Yutaka Nagashima.
    Towards Evolutionary Theorem Proving for Isabelle/HOL.
    arXiv CoRR abs/1904.08468 (2019).
    [ BibTeX | arXiv | dblp ]
82. Yutaka Nagashima.
    LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL.
    arXiv CoRR abs/1906.08084 (2019).
    [ BibTeX | arXiv | dblp ]
83. Yutaka Nagashima.
    Designing Game of Theorems.
    arXiv CoRR abs/1906.08549 (2019).
    [ BibTeX | arXiv | dblp ]
84. Yutaka Nagashima.
    Domain-Specific Language to Encode Induction Heuristics.
    arXiv CoRR abs/1907.02594 (2019).
    [ BibTeX | arXiv | dblp ]
85. Olaf Beyersdorff, Leroy Chew, Mikolás Janota.
    New Resolution-Based QBF Calculi and Their Proof Complexity.
    TOCT 11: 26:1-26:42 (2019).
    [ BibTeX | doi | dblp ]
86. 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).
    [ BibTeX | doi | dblp ]
87. 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).
    [ BibTeX | doi | dblp ]
88. Simon Cooksey, Sarah Harris, Mark Batty, Radu Grigore, Mikolás Janota.
    PrideMM: A Solver for Relaxed Memory Models.
    arXiv CoRR abs/1901.00428 (2019).
    [ BibTeX | arXiv | dblp ]

2018

89. Pascal Fontaine, Cezary Kaliszyk, Stephan Schulz, Josef Urban.
    Foreword to the Special Issue on Automated Reasoning.
    AI Commun. 31: 235-236 (2018).
    [ BibTeX | doi | dblp ]
90. Jan Jakubuv, Josef Urban.
    Hierarchical invention of theorem proving strategies.
    AI Commun. 31: 237-250 (2018).
    [ BibTeX | doi | dblp ]
91. 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).
    [ BibTeX | doi | dblp ]
92. 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).
    [ BibTeX | doi | dblp ]
93. 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).
    [ BibTeX | doi | dblp ]
94. 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).
    [ BibTeX | doi | dblp ]
95. 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).
    [ BibTeX | doi | dblp ]
96. 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).
    [ BibTeX | url | dblp ]
97. 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).
    [ BibTeX | url | dblp ]
98. 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).
    [ BibTeX | doi | dblp ]
99. Bartosz Piotrowski, Josef Urban.
    ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback.
    arXiv CoRR abs/1802.03375 (2018).
    [ BibTeX | arXiv | dblp ]
100. Zarathustra Goertzel, Jan Jakubuv, Stephan Schulz, Josef Urban.
     ProofWatch: Watchlist Guidance for Large Theories in E.
     arXiv CoRR abs/1802.04007 (2018).
     [ BibTeX | arXiv | dblp ]
101. Thibault Gauthier, Cezary Kaliszyk, Josef Urban.
     Learning to Reason with HOL4 tactics.
     arXiv CoRR abs/1804.00595 (2018).
     [ BibTeX | arXiv | dblp ]
102. Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, Michael Norrish.
     Learning to Prove with Tactics.
     arXiv CoRR abs/1804.00596 (2018).
     [ BibTeX | arXiv | dblp ]
103. Michael Färber, Cezary Kaliszyk, Josef Urban.
     Machine Learning Guidance and Proof Certification for Connection Tableaux.
     arXiv CoRR abs/1805.03107 (2018).
     [ BibTeX | arXiv | dblp ]
104. Qingxiang Wang, Cezary Kaliszyk, Josef Urban.
     First Experiments with Neural Translation of Informal to Formal Mathematics.
     arXiv CoRR abs/1805.06502 (2018).
     [ BibTeX | arXiv | dblp ]
105. Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Mirek Olsák.
     Reinforcement Learning of Theorem Proving.
     arXiv CoRR abs/1805.07563 (2018).
     [ BibTeX | arXiv | dblp ]
106. 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).
     [ BibTeX | doi | dblp ]
107. 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).
     [ BibTeX | easychair | dblp ]
108. 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).
     [ BibTeX | easychair | dblp ]
109. 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).
     [ BibTeX | doi | dblp ]
110. 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).
     [ BibTeX | doi | dblp ]
111. Yutaka Nagashima, Julian Parsert.
     Goal-Oriented Conjecturing for Isabelle/HOL.
     arXiv CoRR abs/1806.04774 (2018).
     [ BibTeX | arXiv | dblp ]
112. Yutaka Nagashima, Yilun He.
     PaMpeR: Proof Method Recommendation System for Isabelle/HOL.
     arXiv CoRR abs/1806.07239 (2018).
     [ BibTeX | arXiv | dblp ]
113. Yutaka Nagashima.
     Towards Machine Learning Mathematical Induction.
     arXiv CoRR abs/1812.04088 (2018).
     [ BibTeX | arXiv | dblp ]
114. 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).
     [ BibTeX | url | dblp ]
115. 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).
     [ BibTeX | doi | dblp ]

2017

116. 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).
     [ BibTeX | doi | dblp ]
117. 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).
     [ BibTeX | doi | dblp ]
118. 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).
     [ BibTeX | easychair | dblp ]
119. 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).
     [ BibTeX | easychair | dblp ]
120. 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).
     [ BibTeX | doi | dblp ]
121. 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).
     [ BibTeX | doi | dblp ]
122. 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).
     [ BibTeX | doi | dblp ]
123. 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).
     [ BibTeX | easychair | dblp ]

2016

124. 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).
     [ BibTeX | arXiv | dblp ]
125. Michael Färber, Chad E. Brown.
     Internal Guidance for Satallax.
     arXiv CoRR abs/1605.09293 (2016).
     [ BibTeX | arXiv | dblp ]
126. Jan Jakubuv, Josef Urban.
     BliStrTune: Hierarchical Invention of Theorem Proving Strategies.
     arXiv CoRR abs/1611.08733 (2016).
     [ BibTeX | arXiv | dblp ]
127. Michael Färber, Cezary Kaliszyk, Josef Urban.
     Monte Carlo Connection Prover.
     arXiv CoRR abs/1611.05990 (2016).
     [ BibTeX | arXiv | dblp ]
128. 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).
     [ BibTeX | arXiv | dblp ]
129. Jan Jakubuv, Josef Urban.
     Extending E Prover with Similarity Based Clause Selection Strategies.
     arXiv CoRR abs/1606.03888 (2016).
     [ BibTeX | arXiv | dblp ]
130. Chad E. Brown, Josef Urban.
     Extracting Higher-Order Goals from the Mizar Mathematical Library.
     arXiv CoRR abs/1605.06996 (2016).
     [ BibTeX | arXiv | dblp ]
131. 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).
     [ BibTeX | url | dblp ]
132. 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).
     [ BibTeX | doi | dblp ]
133. 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).
     [ BibTeX | doi | dblp ]
134. 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).
     [ BibTeX | doi | dblp ]
135. 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).
     [ BibTeX | doi | dblp ]
136. Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, Josef Urban.
     Hammering towards QED.
     J. Formalized Reasoning 9(1): 101-148 (2016).
     [ BibTeX | doi | dblp ]
137. John Harrison, Josef Urban, Freek Wiedijk.
     Preface: Twenty Years of the QED Manifesto.
     J. Formalized Reasoning 9(1): 1-2 (2016).
     [ BibTeX | doi | dblp ]
138. 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).
     [ BibTeX | doi | dblp ]
139. 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).
     [ BibTeX | doi | dblp ]

2015

140. 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).
     [ BibTeX | easychair ]
141. 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).
     [ BibTeX | easychair ]
142. 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).
     [ BibTeX | doi | dblp ]
143. Josef Urban.
     BliStr: The Blind Strategymaker.
     Global Conference on Artificial Intelligence, GCAI 2015, Tbilisi, Georgia, October 16-19, 2015: 312-319 (2015).
     [ BibTeX | easychair | dblp ]
144. 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).
     [ BibTeX | doi | dblp ]