Activities

Competitions

Online Systems

Meetings

Visitors

Publications

    2016

  1. 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).
  2. Michael Färber, Chad E. Brown.
    Internal Guidance for Satallax.
    arXiv CoRR abs/1605.09293 (2016).
  3. Jan Jakubuv, Josef Urban.
    BliStrTune: Hierarchical Invention of Theorem Proving Strategies.
    arXiv CoRR abs/1611.08733 (2016).
  4. Michael Färber, Cezary Kaliszyk, Josef Urban.
    Monte Carlo Connection Prover.
    arXiv CoRR abs/1611.05990 (2016).
  5. 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).
  6. Jan Jakubuv, Josef Urban.
    Extending E Prover with Similarity Based Clause Selection Strategies.
    arXiv CoRR abs/1606.03888 (2016).
  7. Chad E. Brown, Josef Urban.
    Extracting Higher-Order Goals from the Mizar Mathematical Library.
    arXiv CoRR abs/1605.06996 (2016).
  8. 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).
  9. 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).
  10. 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).
  11. 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).
  12. 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).
  13. Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, Josef Urban.
    Hammering towards QED.
    J. Formalized Reasoning 9(1): 101-148 (2016).
  14. John Harrison, Josef Urban, Freek Wiedijk.
    Preface: Twenty Years of the QED Manifesto.
    J. Formalized Reasoning 9(1): 1-2 (2016).
  15. 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).
  16. 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).
  17. 2015

  18. 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).
  19. 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).
  20. 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).
  21. Josef Urban.
    BliStr: The Blind Strategymaker.
    Global Conference on Artificial Intelligence, GCAI 2015, Tbilisi, Georgia, October 16-19, 2015: 312-319 (2015).
  22. 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).