Sequent Calculi for Branching Time Temporal Logics of Knowledge and Belief

Article type: Research Article

Authors: Sakalauskaitė, Jūratė

Affiliations: Institute of Mathematics and Informatics, Akademijos 4, 08663 Vilnius, Lithuania, e-mail: [email protected]

Abstract: In this paper we consider branching time temporal logics of knowledge and belief. These logics involve the discrete time linear temporal logic operators “next” and “until” with the branching temporal logic operator “on all paths”. The latter operator is interpreted with respect to a version of the bundle semantics. In addition the temporal logic of knowledge (belief) contains an indexed set of unary modal operators “agent i knows” (“agent i believes”) and it contains the modality of common knowledge (belief). For these logics we present sequent calculi with a restricted cut rule. Thus, we get proof systems where proof-search becomes decidable. The soundness and completeness for these calculi are proved.

Keywords: temporal logics of knowledge and belief, branching time, sequent calculus, restricted cut rule

Journal: Informatica, vol. 18, no. 1, pp. 103-114, 2007