Activities

Competitions

Meetings

Visitors

Publications

    2018

  1. 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).
  2. 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).
  3. Pascal Fontaine, Cezary Kaliszyk, Stephan Schulz, Josef Urban.
    Foreword to the Special Issue on Automated Reasoning.
    AI Commun. 31(3): 235-236 (2018).
  4. 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).
  5. 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).
  6. Jan Jakubuv, Josef Urban.
    Hierarchical invention of theorem proving strategies.
    AI Commun. 31(3): 237-250 (2018).
  7. 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).
  8. 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).
  9. Bartosz Piotrowski, Josef Urban.
    ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback.
    arXiv CoRR abs/1802.03375 (2018).
  10. Zarathustra Goertzel, Jan Jakubuv, Stephan Schulz, Josef Urban.
    ProofWatch: Watchlist Guidance for Large Theories in E.
    arXiv CoRR abs/1802.04007 (2018).
  11. Michael Färber, Cezary Kaliszyk, Josef Urban.
    Machine Learning Guidance and Proof Certification for Connection Tableaux.
    arXiv CoRR abs/1805.03107 (2018).
  12. Qingxiang Wang, Cezary Kaliszyk, Josef Urban.
    First Experiments with Neural Translation of Informal to Formal Mathematics.
    arXiv CoRR abs/1805.06502 (2018).
  13. Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Mirek Olsák.
    Reinforcement Learning of Theorem Proving.
    arXiv CoRR abs/1805.07563 (2018).
  14. Mikoláš Janota, Martin Suda.
    Towards Smarter MACE-style Model Finders.
    LPAR-22, 22st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, November 16-21, 2018: To appear (2018).
  15. Adrián Rebola-Pardo, Martin Suda.
    A Theory of Satisfiability-Preserving Proofs in SAT Solving
    LPAR-22, 22st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, November 16-21, 2018: To appear (2018).
  16. 2017

  17. 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).
  18. 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).
  19. 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).
  20. 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).
  21. 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).
  22. 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).
  23. 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).
  24. 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).
  25. 2016

  26. 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).
  27. Michael Färber, Chad E. Brown.
    Internal Guidance for Satallax.
    arXiv CoRR abs/1605.09293 (2016).
  28. Jan Jakubuv, Josef Urban.
    BliStrTune: Hierarchical Invention of Theorem Proving Strategies.
    arXiv CoRR abs/1611.08733 (2016).
  29. Michael Färber, Cezary Kaliszyk, Josef Urban.
    Monte Carlo Connection Prover.
    arXiv CoRR abs/1611.05990 (2016).
  30. 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).
  31. Jan Jakubuv, Josef Urban.
    Extending E Prover with Similarity Based Clause Selection Strategies.
    arXiv CoRR abs/1606.03888 (2016).
  32. Chad E. Brown, Josef Urban.
    Extracting Higher-Order Goals from the Mizar Mathematical Library.
    arXiv CoRR abs/1605.06996 (2016).
  33. 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).
  34. 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).
  35. 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).
  36. 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).
  37. 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).
  38. Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, Josef Urban.
    Hammering towards QED.
    J. Formalized Reasoning 9(1): 101-148 (2016).
  39. John Harrison, Josef Urban, Freek Wiedijk.
    Preface: Twenty Years of the QED Manifesto.
    J. Formalized Reasoning 9(1): 1-2 (2016).
  40. 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).
  41. 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).
  42. 2015

  43. 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).
  44. 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).
  45. 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).
  46. Josef Urban.
    BliStr: The Blind Strategymaker.
    Global Conference on Artificial Intelligence, GCAI 2015, Tbilisi, Georgia, October 16-19, 2015: 312-319 (2015).
  47. 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).