© 1998 by Oxford University Press
| ||||||||||||||||||||||||||||||||||||||||||||||||||
Original Articles |
Resolution for Temporal Logics of Knowledge
Department of Computing and Mathematics, Manchester Metropolitan University Manchester, Ml 5GD. E-mail: C.DixonM.Fisher{at}doc.mmu.ac.uk
Department of Electronic Engineering, Queen Mary and Westfield College London El 4NS. E-mail: M.J.Wooldridge{at}qmw.ac.uk
A resolution-based proof system for a temporal logic of knowledge is presented and shown to be correct. Such logics are useful for proving properties of distributed and multi-agent systems. Examples are given to illustrate the proof system. An extension of the basic system to the multi-modal case is given and illustrated using the muddy children problem.
Keywords: Temporal logic; logics of knowledge; proof; resolution