• 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.

• 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

Present

Past

• 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