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