Cut-Free Sequent Calculus for Multi-Agent Logic of Common Knowledge

Cut-free sequent calculi are handy tools for backward proof-search of logical formulas or sequents. In the present paper, we introduce a Gentzen-type sequent calculus for the logic of common knowledge. To maintain a deterministic backward proof-search process, we do not include cut or cut-like rules in the introduced calculus. Also, derivation loops are used to define provable sequents and to establish termination of backward proof-search. Using this sound and complete finitary loop-type sequent calculus we construct a decision procedure for the logic of common knowledge. The procedure allows to efficiently determine whether an arbitrary formula or sequent is valid in the logic.