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

Brian Hill () and Francesca Poggiolesi ()
Additional contact information
Francesca Poggiolesi: VUB - Vrije Universiteit Brussel [Bruxelles]

Post-Print from HAL

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.

Keywords: Contraction-free; Cut-free; Propositional Dynamic Logic; Tree-hypersequent; Proof theory (search for similar items in EconPapers)
Date: 2010
References: Add references at CitEc
Citations:

Published in Studia Logica, 2010, 94 (1), pp.47-72. ⟨10.1007/s11225-010-9224-z⟩

There are no downloads for this item, see the EconPapers FAQ for hints about obtaining it.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:hal:journl:hal-00521802

DOI: 10.1007/s11225-010-9224-z

Access Statistics for this paper

More papers in Post-Print from HAL
Bibliographic data for series maintained by CCSD ().