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 条
12345