Multi-type display calculus for Propositional Dynamic Logic
arXiv:1805.09144 · doi:10.1093/logcom/exu064
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 admin note: text overlap with arXiv:1805.07586