Tree-sequent calculi and decision procedures for intuitionistic modal logics

被引:4
|
作者
Galmiche, Didier [1 ]
Salhi, Yakoub [2 ]
机构
[1] Univ Lorraine, LORIA, Campus Sci,BP 239, F-54506 Vandoeuvre Les Nancy, France
[2] Univ Artois, CRIL CNRS UMR 8188, Rue Jean Souvraz SP 18, F-62307 Lens, France
关键词
Proof theory; intuitionistic modal logics; sequent calculus; decidability; SYSTEMS;
D O I
10.1093/logcom/exv039
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
In this article we define label-free sequent calculi for the intuitionistic modal logics obtained from the combinations of the axioms T, B, 4 and 5. These calculi are based on a multi-contextual sequent structure, called Tree-sequent, which allows us to define such calculi for such intuitionistic modal logics. From the calculi defined for the IK, IT, IB4 and ITB logics, we also provide new decision procedures and alternative syntactic proofs of decidability.
引用
收藏
页码:967 / 989
页数:23
相关论文
共 50 条
  • [1] Gentzen sequent calculi for some intuitionistic modal logics
    Lin, Zhe
    Ma, Minghui
    [J]. LOGIC JOURNAL OF THE IGPL, 2019, 27 (04) : 596 - 623
  • [2] Terminating sequent calculi for two intuitionistic modal logics
    Iemhoff, Rosalie
    [J]. JOURNAL OF LOGIC AND COMPUTATION, 2018, 28 (07) : 1701 - 1712
  • [3] Tree-sequent methods for subintuitionistic predicate logics
    Ishigaki, Rye
    Kikuchi, Kentaro
    [J]. AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, PROCEEDINGS, 2007, 4548 : 149 - +
  • [4] Sequent Calculi and Decision Procedures for Weak Modal Systems
    Lavendhomme R.
    Lucas T.
    [J]. Studia Logica, 2000, 66 (1) : 121 - 145
  • [5] Graphical Sequent Calculi for Modal Logics
    Ma, Minghui
    Pietarinen, Ahti-Veikko
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2017, (243): : 91 - 103
  • [6] Modular Sequent Calculi for Classical Modal Logics
    Gilbert, David R.
    Maffezioli, Paolo
    [J]. STUDIA LOGICA, 2015, 103 (01) : 175 - 217
  • [7] Modular Sequent Calculi for Classical Modal Logics
    David R. Gilbert
    Paolo Maffezioli
    [J]. Studia Logica, 2015, 103 : 175 - 217
  • [8] Labelled Sequent Calculi for Inquisitive Modal Logics
    Mueller, Valentin
    [J]. LOGIC, LANGUAGE, INFORMATION, AND COMPUTATION, WOLLIC 2024, 2024, 14672 : 122 - 139
  • [9] Local Intuitionistic Modal Logics and Their Calculi
    Balbiani, Philippe
    Gao, Han
    Gencer, Cigdem
    Olivetti, Nicola
    [J]. AUTOMATED REASONING, IJCAR 2024, PT II, 2024, 14740 : 78 - 96
  • [10] Labeled sequent calculi for modal logics and implicit contractions
    Pierluigi Minari
    [J]. Archive for Mathematical Logic, 2013, 52 : 881 - 907