Sequent Calculi for the Modal μ-Calculus over S5

被引：3
|
作者：
Alberucci, Luca [1 ]
机构：
[1] Univ Bern, CH-3012 Bern, Switzerland
来源：
JOURNAL OF LOGIC AND COMPUTATION | 2009年 / 19卷 / 06期
关键词：
Modal mu-calculus; modal logic; proof-theory; sequent calculus; completeness; COMPLETENESS;
D O I：
10.1093/logcom/exn106
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We present two sequent calculi for the modal mu-calculus over S5 and prove their completeness by using classical methods. One sequent calculus has an analytical cut rule and could be used for a decision procedure the other uses a modified version of the induction rule. We also provide a completeness theorem for Kozen's Axiomatization over S5 without using the completeness result established by Walukiewicz for the modal mu-calculus over arbitrary models.
引用
收藏
页码：971 / 985
页数：15
相关论文
共 50 条
  • [41] Modal sequent calculi labelled with truth values:: Completeness, duality and analyticity
    Mateus, Paulo
    Sernadas, Amilcar
    Sernadas, Cristina
    Vigano, Luca
    [J]. LOGIC JOURNAL OF THE IGPL, 2004, 12 (03) : 227 - 274
  • [42] Evidence reconstruction of epistemic modal logic S5
    Rubtsova, Natalia
    [J]. COMPUTER SCIENCE - THEORY AND APPLICATIONS, 2006, 3967 : 313 - 321
  • [43] A deep inference system for the modal logic S5
    Stouppa P.
    [J]. Studia Logica, 2007, 85 (2) : 199 - 214
  • [44] Labelled Sequent Calculi for Lewis’ Non-normal Propositional Modal Logics
    Matteo Tesi
    [J]. Studia Logica, 2021, 109 : 725 - 757
  • [45] Labelled Sequent Calculi for Lewis' Non-normal Propositional Modal Logics
    Tesi, Matteo
    [J]. STUDIA LOGICA, 2021, 109 (04) : 725 - 757
  • [46] A Dual-Context Sequent Calculus for S4 Modal Lambda-Term Synthesis
    Miranda-Perea, Favio E.
    Omana Silva, Sammantha
    Gonzalez Huesca, Lourdes del Carmen
    [J]. COMPUTACION Y SISTEMAS, 2022, 26 (02): : 787 - 799
  • [47] Ground nonmonotonic modal logic S5:: New results
    Galindo, MO
    Pérez, JAN
    Ramírez, JRA
    Macías, VB
    [J]. JOURNAL OF LOGIC AND COMPUTATION, 2005, 15 (05) : 787 - 813
  • [48] Hypersequential Argumentation Frameworks: An Instantiation in the Modal Logic S5
    Borg, AnneMarie
    Arieli, Ofer
    [J]. PROCEEDINGS OF THE 17TH INTERNATIONAL CONFERENCE ON AUTONOMOUS AGENTS AND MULTIAGENT SYSTEMS (AAMAS' 18), 2018, : 1097 - 1104
  • [49] Two decidable classes of formulas of the modal logic S5
    Norgela S.
    [J]. Lithuanian Mathematical Journal, 2000, 40 (3) : 269 - 276
  • [50] Modal Logic S5 Satisfiability in Answer Set Programming
    Alviano, Mario
    Batsakis, Sotiris
    Baryannis, George
    [J]. THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2021, 21 (05) : 527 - 542
12345