Sequent Calculi for Temporal Logics of Common Knowledge and Belief

Article type: Research Article

Authors: Sakalauskaitė, Jūratė

Affiliations: Institute of Mathematics and Informatics, Akademijos 4, 08663 Vilnius, Lithuania, e-mail: jurates@ktl.mii.lt

Abstract: In this paper we consider two logics: temporal logic of common knowledge and temporal logic of common belief. These logics involve the discrete time linear temporal logic operators “next” and “until”. In addition the first logic contains an indexed set of unary modal operators “agent i knows”, the second one contains an indexed set of unary modal operators “agent i believes”. Also the first logic contains the modality of common knowledge and the second one contains the modality of common belief. For these logics we present sequent calculi with an analytic cut rule. The soundness and completeness for these calculi are proved.

Keywords: agents, temporal logic, common knowledge, common belief, sequent calculus, analytic cut

Journal: Informatica, vol. 17, no. 1, pp. 85-94, 2006