| EPSRC Reference: |
GR/R45376/01 |
| Title: |
Analysis and Mechanisation of Decidable First-Order Temporal Logics |
| Principal Investigator: |
Fisher, Professor M |
| Other Investigators: |
|
| 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 |