• Automated reasoning - is an area of computer science dedicated to understanding different aspects of reasoning in a way that allows the creation of software which allows computers to reason completely or nearly completely, automatically
  • Automated theorem proving - is the proving of mathematical theorems by a computer program.
  • Mizar - is mathematical library which contains c. 8000 definitions and 50000 theorems.
    Is the biggest library of formal mathematics of all time.

Selected Publications

  • System Description: E.T. 0.1.
    Cezary Kaliszyk, Stephan Schulz, Josef Urban, Jiří Vyskočil. CADE 2015: 389-398
  • Efficient Semantic Features for Automated Reasoning over Large Theories.
    Cezary Kaliszyk, Josef Urban, Jiří Vyskočil. IJCAI 2015: 3084-3090
  • Theorem Proving in Large Formal Mathematics as an Emerging AI Field.
    Josef Urban, Jiří Vyskočil. Essays in Memory of William McCune, LNAI 7788: 240-257 (2013)
  • Automatické uvažování (Automated Reasoning).
    Josef Urban, Jiří Vyskočil, Petr Štěpánek. In Olga Štěpánková et al., editor, Umělá Inteligence 6 (Artificial Intelligence 6), book chapter: 249-278 (2013)
  • MaLeCoP: Machine Learning Connection Prover.
    Josef Urban, Jiří Vyskočil, Petr Štěpánek. TABLEAUX 2011: 263-277
  • Automated Proof Compression by Invention of New Definitions.
    Jiří Vyskočil, David Stanovský, Josef Urban. LPAR (Dakar) 2010: 447-462
  • MaLARea SG1-Machine Learner for Automated Reasoning with Semantic Guidance.
    Josef Urban, Geoff Sutcliffe, Petr Pudlák, Jiří Vyskočil. IJCAR 2008: 441-456





  • ARG - The Prague Automated Reasoning Group
  • Mizar project - Mizar mathematical library
  • CIIRC - Czech Institute of Informatics, Robotics, and Cybernetics
  • TPTP - is a library of test problems for ATP systems


RNDr. Jiří Vyskočil, Ph.D.

Czech Institute of Informatics, Robotics, and Cybernetics
Czech Technical University in Prague
Zikova 1903/4
166 36 Prague 6
Czech Republic

e-mail: vyskoji1 (at)