Resolution Based Theorem Proving for Temporal Logics of Knowledge and Belief with Interactions

This is a 36 month EPSRC funded project which started in August 1999 and finished in February 2003.

People Involved

The Project Abstract

The aim of this project is to develop practical and efficient theorem proving techniques 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 systems 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 resolution based methods for temporal logics of knowledge with interactions are developed and implemented. We have also developed resolution based methods for other combinations of temporal and modal logics. Tableaux based methods for temporal logics of knowledge have also been defined. As the complexity of logics allowing these interactions is high, strategies and heuristics to guide the proof search are essential. These have been focused on the temporal aspects of the system including the development of new algorithms to apply the complex temporal resolution rule and the definition of a Set of Support for temporal resolution. Prototype implementations for these algorithms have been developed.

Further Information

Here summary of the project proposal and here is a summary of the final report.

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