Resolution for temporal logics of knowledge

C. Dixon; M. Fisher; M. Wooldridge

doi:10.1093/logcom/8.3.345

Resolution for temporal logics of knowledge

C. Dixon, M. Fisher, M. Wooldridge

Formal Methods

Research output: Contribution to journal › Article › peer-review

Abstract

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’.

Original language	English
Pages (from-to)	345-372
Number of pages	28
Journal	Journal of Logic and Computation
Volume	8
Issue number	3
DOIs	https://doi.org/10.1093/logcom/8.3.345
Publication status	Published - 1 Jun 1998

Access to Document

10.1093/logcom/8.3.345

Cite this

@article{0c15b730417249a1a53cabb01f0f19d1,

title = "Resolution for temporal logics of knowledge",

abstract = "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 {\textquoteleft}muddy children problem{\textquoteright}.",

author = "C. Dixon and M. Fisher and M. Wooldridge",

year = "1998",

month = jun,

day = "1",

doi = "10.1093/logcom/8.3.345",

language = "English",

volume = "8",

pages = "345--372",

journal = "Journal of Logic and Computation",

issn = "0955-792X",

publisher = "Oxford University Press",

number = "3",

}

TY - JOUR

T1 - Resolution for temporal logics of knowledge

AU - Dixon, C.

AU - Fisher, M.

AU - Wooldridge, M.

PY - 1998/6/1

Y1 - 1998/6/1

N2 - 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’.

AB - 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’.

UR - http://www.scopus.com/inward/record.url?eid=2-s2.0-0032093567&partnerID=MN8TOARS

U2 - 10.1093/logcom/8.3.345

DO - 10.1093/logcom/8.3.345

M3 - Article

SN - 0955-792X

VL - 8

SP - 345

EP - 372

JO - Journal of Logic and Computation

JF - Journal of Logic and Computation

IS - 3

ER -

Resolution for temporal logics of knowledge

Abstract

Access to Document

Other files and links

Fingerprint

Cite this