Sequent calculi for branching time temporal logics of knowledge and beliefwith awareness: Completeness and decidability |
| |
Authors: | J Sakalauskaitė |
| |
Institution: | (1) Institute of Mathematics and Informatics, Akademijos 4, LT-08663 Vilnius, Lithuania |
| |
Abstract: | In this paper, we consider branching time temporal logic CT L with epistemic modalities for knowledge (belief) and with awareness operators. These logics involve the discrete-time linear
temporal logic operators “next” and “until” with the branching temporal logic operator “on all paths”. In addition, the temporal
logic of knowledge (belief) contains an indexed set of unary modal operators “agent i knows” (“agent i believes”). In a language of these logics, there are awareness operators. 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.
Published in Lietuvos Matematikos Rinkinys, Vol. 47, No. 3, pp. 328–340, July–September, 2007. |
| |
Keywords: | temporal logics of knowlwdge and belief branching time sequent calculus awareness |
本文献已被 SpringerLink 等数据库收录! |
|