Automated reasoning is a branch of artificial intelligence dedicated to the study and development of systems capable of producing exact solutions to a problem described in a specific constraint language. Applications of such systems are based on the declarative approach to problem-solving, where the exponential search space of a given problem is implicitly described using logical or mathematical constraints. This approach allows for solving many different computationally challenging problems with a single system.
Modern logic-based reasoning systems are also capable of producing proofs for non-existence of solutions. This property is vital in application areas where correctness is a fundamental requirement, such as hardware and software verification. On the other hand, constraint optimization covers situations where one is interested in finding the best possible solution according to some criteria. Applications based on the declarative approach allow, for example, to conserve resources as efficiently as possible.
Since 2022, I have worked on a postdoctoral project funded by the Research Council of Finland at the Department of Computer Science of the University of Helsinki. My research focuses on the development of incremental logic-based reasoning and optimization procedures for solving computationally challenging problems. Currently, I study applications of such methods for computational problems arising from social choice, formal argumentation, as well as logical inconsistency.