Sequent Calculi for Branching Time Temporal Logics of Knowledge and Belief

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. Key words: temporal logics of knowledge and belief, branching time, sequent calculus, restricted cut rule.

• Type: Journal
• Year: 2007
• Where: INFORMATICALT
• Authors: Jurate Sakalauskaite
• Keywords: INFORMATICALT 2007, Temporal Logic Operator, Temporal Logics, Time Temporal Logics