EPSRC logo

Details of Grant 

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:
Artificial Intelligence
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