We are an international research group working on various aspects of Automated Reasoning, AI, and Machine Learning. Our focus is on Automated and Interactive Theorem Proving, SMT solving, and Formalisation of Mathematics.

We have pioneered combinations and cross-fertilisation of these fields with Machine Learning and related AI fields, and developed some of the first benchmarks, feedback loops and other methods combining learning, theorem proving and automated formalisation. Our systems have won a number of competitions in automated reasoning and the methods developed by us today assist formal verification in various environments. The AI4REASON ERC Consolidator project led by Josef Urban has been the first ERC-funded AI project in Czechia, and also the first ERC project at CTU. Other projects include the ERC-CZ funded POSTMAN by Mikolas Janota combining SMT and learning methods, a GACR-funded project on improving theorem provers by machine and reinforcement learning by Martin Suda, and a large national (EU-supported) Excellent Teams project addressing AI and Reasoning (PI J. Urban). Josef Urban also serves on the CLAIRE Extended Core Team. The group is part of the Intelligent Systems Department at CIIRC CTU – a university institute of the Czech Technical University in Prague (CTU) focused on computer science, AI and robotics.

Facts & Figures 

• 11 members: 4 senior researchers, 4 postdocs, 5 PhD students 
• Annual budget: 400k EUR
• Areas of AI research:
  • Machine Learning
  • Automated Reasoning
  • Search and Optimisation
  • Planning and Scheduling
  • Knowledge Representation 
  • Natural Language Processing
• Areas of AI applications 
  • accelerated scientific research
  • safety and security
• Contact 
  • Josef Urban, Distinguished Researcher – Josef.Urban(at)gmail.com
  • Mikolas Janota, Senior Researcher – Mikolas.Janota(at)gmail.com
  • Martin Suda, Senior Researcher  – Martin.Suda(a)gmail.com

(as of September 2021)