Cut-elimination for knowledge logics with interaction

Abstract

In the article, multimodal logics K4_n and S4_n with the central agent axiom are analysed. The Hilbert type calculi are presented, then the Gentzen type calculi with cut are derived, and the proofs of the
cut-eliminationtheorems are outlined. The work shows that it is possible to construct an analytical Gentzen type calculi for these logics.