| EPSRC Reference: |
GR/M44859/02 |
| Title: |
RESOLUTION BASED THEOREM-PROVING FOR TEMPORAL LOGICS OF KNOWLEDGE AND BELIEF WITH INTERACTIONS |
| Principal Investigator: |
Dixon, Professor C |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
University of Liverpool |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 January 2001 |
Ends: |
28 February 2003 |
Value (£): |
29,602
|
| EPSRC Research Topic Classifications: |
|
| 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 develop a practical and efficient theorem prover for temporal logics of knowledge and belief with interactions. Such logics are useful for the verification of distributed and multi-agent system, both of which are becoming increasingly important in computer science yet are complex and difficult to design and implement. While temporal logics of knowledge and belief are widely used in the specification and verification of such system, little work has been carried out in developing their proof methods.A novel method to apply clausal resolution to temporal logics has been developed and extended to temporal logics of knowledge and belief. In its basic form, interactions between the dimensions of knowledge or belief and time are not allowed and consequently, systems cannot be considered where knowledge evolves over time.In this project algorithms to apply resolution rules allowing such interactions are developed and implemented. As the complexity of logics allowing these interactions is high, strategies and heuristics to guide the proof search are essential. These are to be developed, their theoretical properties examined and then implemented. The resulting theorem prover will be tested on a selection of case studies.
|
|
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 |