Analysis and Mechanisation of Decidable First-Order Temporal Logics

This is a 30 month EPSRC funded project which started in November 2001 in London and in March 2002 in Liverpool. The London part of the project ended 31st March 2004 and the Liverpool part ended on 3rd April 2005.

Collaborators

The Project

In this project we will investigate FOTL in depth, and develop, implement, and analyse tools mechanising the axiomatisable and decidable fragments of FOTL identified. Further details of the project are available.

Papers and Reports Related to the Project

Here are details of papers relating to work carried out on the project.

Here is the project final report.