AUTOPROVING
Automated Theorem Proving from the Mindset of Parameterized Complexity Theory
A project financed by the Research Council of Norway, under the IKTPLUS Young Research Talents Initiative.
Mateus de Oliveira Oliveira
Welcome to the webpage of the project AUTOPROVING. This is a project financed by the Research Council of Norway under the IKTPLUSS Young Research Talents program (8 Million NOK). Our goal is to advance the field of automated theorem proving by employing techniques from the field of parameterized complexity theory.
24/June/2021 – I’m happy to announce that my second project, Symbolic Algorithms: A parameterized Approach (SYMBOALGO), has been granted funding of 12 Million NOK by the Research Council of Norway under the FRIPRO Ground-Breaking Research program. The goal of this project is to solve important challenges in the field of artificial intelligence using the framework of symbolic algorithms.
Automated Theorem Proving from the Mindset of Parameterized Complexity Theory
The idea of proving or disproving mathematical statements using automated procedures has been contemplated for at least one century. Nevertheless, even though the field of automated reasoning has reached important milestones during the past few decades, the question of whether computers can significantly speed up the process of proof construction remains elusive.
The goal of this project is to identify a series of numerical parameters that are typically small in humanly produced proofs. Intuitively these parameters are intended to provide a numerical quantification of the complexity of a proof. Using information about these parameters, we will develop new algorithms that will be able to either find a proof of a given predetermined complexity or to determine that no such proof exists.
As a byproduct, we expect that our results will have the potential to improve significantly the automation capabilities of a variety of tools, such as proof assistants, software verification tools, specialist systems, etc.