Tilbake til søkeresultatene

IKTPLUSS-IKT og digital innovasjon

Automated Theorem Proving from the Mindset of Parameterized Complexity Theory

Alternativ tittel: Automatisert beviskonstruksjon inspirert av parameterisert kompleksitetsteori

Tildelt: kr 8,0 mill.

Å bevise eller motbevise matematiske setninger ved hjelp av automatiserte prosedyrer har vært en appellerende idé i minst et århundre. Likevel, selv om forskingsfeltet om automatiserte resonnement har nådd viktige milepæler de siste tiårene, er det fortsatt uavklart hvorvidt datamaskiner i vesentlig grad kan øke hastigheten på prosessen med beviskonstruksjon. Målet med dette prosjektet er å identifisere en rekke numeriske parametere som vanligvis er små i menneskelig produserte bevis. Intuitivt er disse parametrene ment å gi en numerisk kvantifisering av kompleksiteten til et bevis. Ved å bruke informasjon om disse parameterne, vil vi utvikle nye algoritmer som vil kunne enten finne et bevis med en gitt forutbestemt kompleksitet, eller å fastslå at det ikke finnes noe slikt bevis. Som et biprodukt forventer vi at resultatene våre vil kunne forbedre automasjonskapasiteten til en rekke verktøy, for eksempel bevisassistenter, programvareverifikasjonsverktøy og lignende.

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.

Budsjettformål:

IKTPLUSS-IKT og digital innovasjon