Skip to Main content Skip to Navigation
Journal articles

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

Brian Hill 1 Francesca Poggiolesi 2
1 GREGH - Groupement de Recherche et d'Etudes en Gestion à HEC
2 VUB - Vrije Universiteit Brussel
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
Document type :
Journal articles
Complete list of metadatas
https://hal-hec.archives-ouvertes.fr/hal-00521802
Contributor : Antoine Haldemann <>
Submitted on : Tuesday, September 28, 2010 - 3:31:39 PM
Last modification on : Thursday, June 4, 2020 - 11:46:02 AM

Links full text

openaccess

Identifiers

Collections

HEC | PARISTECH | CNRS

Citation

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

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

252