Multi-type display calculus for Propositional Dynamic Logic
Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra, Palmigiano
TL;DR
This paper presents a new multi-type display calculus for Propositional Dynamic Logic that is complete, cut-eliminating, and maintains the subformula property, enhancing proof-theoretic analysis of PDL.
Contribution
The paper introduces a novel multi-type display calculus for PDL with proven completeness, cut-elimination, and subformula property, advancing proof-theoretic methods for dynamic logic.
Findings
Complete calculus for PDL established
Cut-elimination property proven
Subformula property maintained
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.