Automated 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
See http://ai4reason.org/ for more details.
Contact Person
Josef Urban
josef.urban@cvut.cz
