@inproceedings{9523f74e1b024d238805622af4164836,
title = "A resolution-based proof method for temporal logics of knowledge and belief",
abstract = "In this paper we define two logics, KLn and BLn, and present resolution-based proof methods for both. KLn is a temporal logic of knowledge. Thus, in addition to the usual connectives of linear discrete temporal logic, it contains a set of unary modal connectives for representing the knowledge possessed by agents. The logic BLn is somewhat similar: it is a temporal logic that contains connectives for representing the beliefs of agents. The proof methods we present for these logics involve two key steps. First, a formula to be tested for unsatisfiability is translated into a normal form. Secondly, a family of resolution rules are used, to deal with the interactions between the various operators of the logics. In addition to a description of the normal form and the proof methods, we present some short worked examples and proposals for future work.",
author = "M. Fisher and M. Wooldridge and C. Dixon",
year = "1996",
doi = "10.1007/3-540-61313-7\_72",
language = "English",
isbn = "978-3-540-61313-8",
series = "Lecture Notes in Computer Science",
publisher = "Springer Nature",
pages = "178--192",
booktitle = "Practical Reasoning",
address = "United States",
note = "FAPR : International Conference on Formal and Applied Practical Reasoning ; Conference date: 03-06-1996 Through 07-06-1996",
}