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 infini-
tary 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.
built using an enriched version of the tree-hypersequent method and including an infini-
tary 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.
| Original language | English |
|---|---|
| Pages (from-to) | 69-94 |
| Number of pages | 25 |
| Journal | Studia Logica |
| Volume | 94 |
| Publication status | Published - 10 Feb 2010 |
Keywords
- tree-hypersequent, propositional dynamic logic