A Contraction-free and Cut-free Sequent Calculus for Propositional Dynamic Logic

被引：0
|
作者：
Brian Hill
Francesca Poggiolesi
机构：
[1] Vrije Universiteit Brussel,Center of Logic and Philosophy of Science (CLFW)
[2] HEC Paris and IHPST (CNRS / Paris 1 / ENS),undefined
来源：
Studia Logica | 2010年 / 94卷
关键词：
Contraction-free; Cut-free; Propositional Dynamic Logic; Tree-hypersequent; Proof theory;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
In this paper we present a sequent calculus for propositional dynamic logic built using an enriched version of the tree-hypersequent method and including an infinitary rule for the iteration operator. We prove that this sequent calculus is theoremwise equivalent to the corresponding Hilbert-style system, and that it is contraction-free and cut-free. All results are proved in a purely syntactic way.
引用
收藏
页码：47 / 72
页数：25
相关论文
共 50 条
  • [1] A Contraction-free and Cut-free Sequent Calculus for Propositional Dynamic Logic
    Hill, B.
    Poggiolesi, F.
    [J]. STUDIA LOGICA, 2010, 94 (01) : 47 - 72
  • [2] A cut-free labelled sequent calculus for dynamic epistemic logic
    Nomura, Shoshin
    Ono, Hiroakira
    Sano, Katsuhiko
    [J]. JOURNAL OF LOGIC AND COMPUTATION, 2020, 30 (01) : 321 - 348
  • [3] A Cut-Free Labelled Sequent Calculus for Dynamic Epistemic Logic
    Nomura, Shoshin
    Ono, Hiroakira
    Sano, Katsuhiko
    [J]. LOGICAL FOUNDATIONS OF COMPUTER SCIENCE (LFCS 2016), 2016, 9537 : 283 - 298
  • [4] A cut-free sequent calculus for relevant logic RW*
    Ilic, Mirjana
    Boricici, Branislav
    [J]. LOGIC JOURNAL OF THE IGPL, 2014, 22 (04) : 673 - 695
  • [5] A cut-free sequent calculus for Bi-intuitionistic logic
    Buismani, Linda
    Gore, Rajeev
    [J]. AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, PROCEEDINGS, 2007, 4548 : 90 - +
  • [6] Cut-free Sequent Calculus and Natural Deduction for the Tetravalent Modal Logic
    Martín Figallo
    [J]. Studia Logica, 2021, 109 : 1347 - 1373
  • [7] Cut-free Sequent Calculus and Natural Deduction for the Tetravalent Modal Logic
    Figallo, Martin
    [J]. STUDIA LOGICA, 2021, 109 (06) : 1347 - 1373
  • [8] CONTRACTION-FREE SEQUENT CALCULI FOR INTUITIONISTIC LOGIC
    DYCKHOFF, R
    [J]. JOURNAL OF SYMBOLIC LOGIC, 1992, 57 (03) : 795 - 807
  • [9] ON THE CUT-FREE SEQUENT CALCULUS FOR THE LOGIC OF THE WEAK LAW OF EXCLUDED MIDDLE
    BORICIC, BR
    [J]. JOURNAL OF SYMBOLIC LOGIC, 1987, 52 (01) : 309 - 309
  • [10] A PURELY SYNTACTIC AND CUT-FREE SEQUENT CALCULUS FOR THE MODAL LOGIC OF PROVABILITY
    Poggiolesi, Francesca
    [J]. REVIEW OF SYMBOLIC LOGIC, 2009, 2 (04): : 593 - 611
12345