View Project

Norwegian AI Directory

Automated Theorem Proving from the Mindset of Parameterized Complexity Theory


Description:

Å 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.


Project leader: Mateus de Oliveira Oliveira

Started: 2019

Ends: 2023

Category: Universiteter

Sector: UoH-sektor

Budget: 7999980

Institution: UNIVERSITETET I BERGEN

Address: