Multi-type display calculus for propositional dynamic logic

Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano

Research output: Contribution to journalArticleScientificpeer-review

19 Citations (Scopus)


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.

Original languageEnglish
Pages (from-to)2067-2104
Number of pages38
JournalJournal of Logic and Computation
Issue number6
Publication statusPublished - 2016


  • Display calculus
  • Multi-type proof-system
  • Propositional dynamic logic

Fingerprint Dive into the research topics of 'Multi-type display calculus for propositional dynamic logic'. Together they form a unique fingerprint.

Cite this