Research activities of the AIF group focus on different aspects of artificial intelligence and computational logic, namely automated reasoning, interactive theorem proving and working with large formal (mainly mathematical) knowledge bases (KBs). It involves automated deductive reasoning (automated theorem proving), inductive reasoning (machine learning and discovery) and their combining. We are also quite involved in formalization, computer-verification, typing, model checking and declarative and functional programming.
In recent years, we have started developing a new methods for natural language processing in well formalizable domains like mathematics and computer science.
Responsible: Jiří Vyskočil