A Contraction-free and Cut-free Sequent Calculus for Propositional Dynamic Logic - HEC Paris - École des hautes études commerciales de Paris Access content directly
Journal Articles Studia Logica Year : 2010

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

Francesca Poggiolesi

Abstract

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.

Dates and versions

hal-00521802 , version 1 (28-09-2010)

Identifiers

Cite

Brian Hill, Francesca Poggiolesi. A Contraction-free and Cut-free Sequent Calculus for Propositional Dynamic Logic. Studia Logica, 2010, 94 (1), pp.47-72. ⟨10.1007/s11225-010-9224-z⟩. ⟨hal-00521802⟩

Collections

HEC CNRS
63 View
0 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More