A cut free tableau calculus for the logic of common knowledge




In this paper we focus on the development of a cut-free finitary tableau calculus with histories for n-agent modal logics with common knowledge (LCK). Thus, we get a proof system where proof-search becomes feasible and we lay the basis for developing a uniform framework for the treatment of the family of logics of common knowledge. Unlike two-pass decision methods like those for temporal logics, our calculus gives a single-pass decision procedure which is space-optimal.