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.

Project Participants

Software

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. 

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.

Scroll to Top