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

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.

• Type: Journal
• Year: 2010
• Where: SLOGICA
• Authors: Brian Hill, Francesca Poggiolesi
• Keywords: Data Mining, Infinitary Rule, Propositional Dynamic Logic, Sequent Calculus, SLOGICA 2010