Cirkulära resonemang: en undersökning om icke-välgrundade bevis

Projektet handlar om icke-välgrundade och cirkulära bevissystem, i synnerhet i samband med fixpunktlogiker. Det vanliga synsättet inom bevisteori är att betrakta ett bevis som en ändlig, välgrundad struktur, i vilken slutsatsen rättfärdigas av en kedja härledningssteg som slutligen grundas i något axiom.

I icke-välgrundade bevis tillåts oändliga kedjor av härledningssteg eller cykler där det som ska härledas också antas som premiss. Istället för att grundas i axiom, så betraktas sådana bevis som giltiga eller ej beroende på globala villkor för strukturen hos ett bevis. Icke-välgrundade bevissystem har visat sig vara kraftfulla verktyg för att hantera induktion och ko-induktion.

Syftet med det här projektet är att följa upp på nya utvecklingar inom området, med sikte på att utveckla fullständiga bevissystem för modala fixpunktlogiker, särskilt extensioner till modal mu-calculus.