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

作者：Hill B^*; Poggiolesi F

来源：Studia Logica, 2010, 94(1): 47-72.

DOI：10.1007/s11225-010-9224-z

• Contraction-free
• Cut-free
• Propositional Dynamic Logic
• Tree-hypersequent
• Proof theory

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 theoremwisc 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.

• 出版日期2010-2
• 单位HEC Paris