Multi-type display calculus for Propositional Dynamic Logic

Abstract

We introduce a multi-type display calculus for Propositional Dynamic Logic (PDL). This calculus is complete w.r.t. PDL, and enjoys Belnap-style cut-elimination and subformula property.

arXiv commentarXiv admin note: text overlap with arXiv:1805.07586

References in corpus (4)

• Multi-type Display Calculus for Dynamic Epistemic Logic
• A Proof-Theoretic Semantic Analysis of Dynamic Epistemic Logic
• Multi-type Sequent Calculi
• Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic -- Extended Version

Cited by in corpus (14)

• Multi-type Display Calculus for Dynamic Epistemic Logic
• A Proof-Theoretic Semantic Analysis of Dynamic Epistemic Logic
• Toward an Epistemic-Logical Theory of Categorization
• Multi-type Sequent Calculi
• Algebraic proof theory for LE-logics
• The Logic of Resources and Capabilities
• Non normal logics: semantic analysis and proof theory
• Structural Multi-type Sequent Calculus for Inquisitive Logic
• Unified Correspondence as a Proof-Theoretic Tool
• Kleene algebras, adjunction and structural control
• First order logic properly displayed
• Tool support for reasoning in display calculi
• Non-normal logics: semantic analysis and proof theory (extended version)
• Completeness for Game Logic