Taming Jörmungandr: The Logical Foundations of Circularity
Kort beskrivning
Forskningsprogrammet kommer att utveckla ett enhetligt ramverk för teorin om och tillämpningen av cykliska bevis. Vi kommer att ta upp grundläggande frågor om de cykliska bevisens natur: Vad avslöjar cykliska bevis om våra matematiska och filosofiska ramverk? Hur kan de användas för att effektivisera algoritmer och beräkningar? Är cykliska bevis den felande länken som förklarar de djuplodande likheterna mellan matematisk induktion och datavetenskaplig rekursion?
Cykliska bevis lägger ett nytt perspektiv, som inte finns i traditionella bevisformalismer, till vår förståelse av bevisbarhet. De representerar dess dynamiska aspekt: verifieringar av icke-terminerande processer och vinnande strategier i oändliga spel. Logisk-lingvistiska begrepp som kännetecknas av självreferens, inklusive temporalitet och sanning, kan relateras till cykliska bevisformer, vilket ger en formell grund för deras analys. Datoralgoritmer kan utformas för att söka efter cykler i resonemang, vilket ger oss algoritmer för automatiserad korrektursökning och certifiering av säkerhetskritiska system.
Detta forskningsprojekt syftar till att utveckla ett enhetligt ramverk för studiet av cirkularitet både i teorin och för tillämpningar, med särskilt fokus på tre områden:
Enhetliga metoder för att framställa och analysera cykliska och icke-välgrundade härledningssystem, inklusive allmänna korrekthetsargument, normalformer och översättningar till/från ändliga bevis.
Fördjupning av vår förståelse av sanning och ontologi i matematik, särskilt i relation till olika former av bevisbarhet, berättigande och verifiering.
Formella karaktäriseringar av likhet, likformighet och ekvivalens som moderna framsteg inom matematik, filosofi och datavetenskap bygger på.
För mer information om projektet se projektets engelskspråkiga webbsida
https://www.gu.se/en/research/taming-jormungandr-the-logical-foundations-of-circularity-0