AR: Automatic reasoning

Our goal is to develop strong AI and automated reasoning (AR) systems capable of assisting mathematics, science, and the development of formally verified software and designs. Our focus is on combining AR with machine learning (ML) and cross-fertilization of inductive and deductive AI methods, in particular over large formal mathematical and verification corpora.

Research topics include:

  • learning-guided automated theorem proving,
  • SAT, QBF, and SMT solving, their combinations with ML,
  • AI metasystems interleaving learning and reasoning,
  • formalization and interactive theorem proving, its automation, assistance, and autoformalization

Projects: AI4Reason, PowerATP

Find more info on the web of our group

Head of the group

Name: Martin Suda

PIs: Josef Urban, Martin Suda

Staff: Chad Brown, Jan Jakubův, Thibault Gauthier, Karel Chvalovský, Jan Hůla, Robert Veroff (affiliated research professor)

PhD students: Filip Bártek, Lasse Blaauwbroek, Zarathustra Goertzel, Yutaka Nagashima, Jelle Piepenbrock, Bartosz Piotrowski