 |
 |
 |
Journal articles
A Contraction-free and Cut-free Sequent Calculus for Propositional Dynamic Logic
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.
https://hal-hec.archives-ouvertes.fr/hal-00521802
Contributor : Antoine Haldemann Connect in order to contact the contributor
Submitted on : Tuesday, September 28, 2010 - 3:31:39 PM
Last modification on : Wednesday, June 2, 2021 - 4:20:02 PM
Contributor : Antoine Haldemann Connect in order to contact the contributor
Submitted on : Tuesday, September 28, 2010 - 3:31:39 PM
Last modification on : Wednesday, June 2, 2021 - 4:20:02 PM
Links full text
