Home Online Resources Table of Contents

Journal of Logic and Computation, Volume 8, Issue 3: June 1998.

Resolution for temporal logics of knowledge

C Dixon1, M Fisher1 and M Wooldridge2

1Department of Computing and Mathematics, Manchester Metropolitan University, Manchester M1 5GD, UK, E-mail: {C.Dixon,M.Fisher@doc.mmu.ac.uk}, 2Department of Electronic Engineering, Queen Mary and Westfield College, London E1 4NS, UK, E-mail: M.J.Wooldridge@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.

Pages 345-372

This page is run by Oxford University Press, Great Clarendon Street, Oxford OX2 6DP, UK
as part of the OUP Journals World Wide Web service.
Comments and feedback: www-admin@oup.co.uk
URL: http://www.oup.co.uk/logcom/hdb/Volume_08/Issue_03/080345.sgm.abs.html
Last modification: 22 July 1998.
Copyright© Oxford University Press, 1998.