EPSRC logo

Details of Grant 

EPSRC Reference: GR/R45376/01
Title: Analysis and Mechanisation of Decidable First-Order Temporal Logics
Principal Investigator: Fisher, Professor M
Other Investigators:
Dixon, Professor C Wolter, Professor F Hustadt, Dr U
Researcher Co-Investigators:
Project Partners:
Department: Computer Science
Organisation: University of Liverpool
Scheme: Standard Research (Pre-FEC)
Starts: 04 March 2002 Ends: 03 April 2005 Value (£): 148,162
EPSRC Research Topic Classifications:
Artificial Intelligence Fundamentals of Computing
EPSRC Industrial Sector Classifications:
No relevance to Underpinning Sectors
Related Grants:
Panel History:  
Summary on Grant Application Form
The aim of this project is to analyse, in depth, monodic FOTL and its decidable extensions, and to develop, implement and apply methods of automated deduction for the constructed temporal formalisms. Thus, this project will combine work on logical and computational properties of wellbehaved fragments of FOTL (Gabbay, Hodkinson, Kurucz, Zakharyaschev) with work on the theory, implementation and application of temporal verification methods (Degtyarev, Dixon, Fisher). It will extend and enhance both areas. The new work on monodic fragments of FOTL has opened up a range of important opportunities and it is our aim to follow these up as soon as possible, providing significant advances in the area of temporal verification.The work comprising this project constitutes a natural and feasible extension to our ongoing work and brings together two of the world's foremost research teams. In addition, this project complements the ongoing EPSRC project on Mechanising First-Order Temporal Logic (GR/M46631), being carried out between Liverpool (Fisher, Quigley) and Edinburgh (Smaill, Bundy), which is tackling the undecidable/non-enumerable parts of FOTL using inductive proof techniques and proof planning.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Summary
Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:  
Further Information:  
Organisation Website: http://www.liv.ac.uk