Temporal logic(s) in Agda

Potential supervisors: 
Description: 

 

The goal of this project will first be to prove in Agda that LTL (linear-time temporal logics) is decidable.

Hopefully, this will be feasible relatively quickly (but non trivial since the usual arguments use classical logic) and the next step will be to prove that the logic S1S of second order monadic logic with successor is decidable.

The usual proof uses classical logic and Ramsey theorem so it cannot be used in Agda as such. There are strong hopes that using the techniques presented in the following papers, we should be able to do it in Agda.

References: http://logicatorino.altervista.org/steila/slides/Vienna2014PSC.pdf and http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.225.3021

 

Prerequisites: Familiarity with Agda and type theory or having taken the course DAT350/DIT233 Types for programs and proofs.The project is suitable for 1 or 2 students.

Contact: Thierry Coquand thierry.coquand@cse.gu.se

Date range: 
October, 2020 to October, 2024