This project investigates the possibilities of automated reasoning from a theoretical point of view. It was proven in the 1930s that it is impossible to fully automate all mathematical reasoning, and since then, mathematicians and logicians have worked for identifying sufficiently restricted frameworks where automatization can in fact be carried out. This project contributes to the current trends of the related theory. The goal is to identify different automatic frameworks, or logics, for different purposes. More expressive logics are slower to reason with than weaker ones, so there is a trade-off between expressivity and speed of use. The project builds a unified theory that helps to better understand the strengths and weaknesses of different logics and enables different logics to be compared with each other.

2019

2024