Norwegian AI Directory
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: NA