Proof Methods for Temporal Logics of Knowledge and Belief

Grantholders:

Funding

EPSRC research grant GR/K57282, funded for three years from December 1995.

Research Staff

Clare Dixon was employed as the research fellow on the project from December 1995 until August 1997 (21 months). She was then included as a co-investigator on her appointment as a research lecturer at MMU. Following a six month break, Ullrich Hustadt was then appointed for the last 15 months of the project. Adam Kellett was employed as a technician on the project for 12 months, involved in the implementation of the Clatter system. Michael Wooldridge, an original co-investigator, spent a number of months working in industry during the middle of the project period.

Project Abstract

The aim of this project is to develop and evaluate proof methods for temporal logics that incorporate connectives operating over the dimensions of both knowledge and belief. Such logics are exploited in a variety of application areas, but particularly in distributed and multi-agent systems, where they are used for specification and verification. Both of these types of systems are themselves becoming increasingly important in both mainstream computer science and AI. Thus, the development of proof methods for such logics will ultimately contribute greatly to the development of distributed and multi-agent systems. The project will combine work on proof methods for temporal logics (such as our recently developed clausal resolution method) with work on proof methods for normal modal logics. Specifically, the project will develop tableau methods, resolution-style calculi, and various translation methods for temporal epistemic and doxastic logics. These methods will be evaluated with respect to both their theoretical complexity and their suitability for implementation. Those proof methods that appear best-suited to automation will be prototyped, applied to problems relating to the specification and verification of distributed and multi-agent systems, and evaluated with respect to both their theoretical complexity and demonstrated efficiency.

Final report

A summary of the final report of the project is available here. For further details relating to this project contact: 
  Michael Fisher
  Department of Computer Science
  University of Liverpool
  Liverpool L69 7ZF
  United Kingdom

  email M.Fisher@csc.liv.ac.uk


  tel   (+44 161) 794 6701


  fax   (+44 161) 794 3715
Last modified: Wed Feb 28 2001 . © 2001 by Michael Fisher, Clare Dixon, Ullrich Hustadt.