Temporal logic of common knowledge and its resolution-based proof method.

The purpose of the current article is to introduce a propositional linear time temporal logic of common knowledge. This logic can be utilized for reasoning when the agents should commonly know the information that may change over time. This is the main advantage of our logic over the existing temporal logics of knowledge in the literature. We provide a language, as well as appropriate semantics for our logic. We also introduce a resolution-based proof method for this logic by adopting the approach proposed by Dixon et al. [11, 14]. This resolution system is based upon a separated normal form. We prove that our resolution system is sound and complete. More importantly, to justify our approach, we apply our resolution method to specify and verify the anonymity properties of Chaum's dining cryptographers protocol [4]. [ABSTRACT FROM AUTHOR]