Multi-type display calculus for propositional dynamic logic

G. Greco; Sabine Frittella; Alexander Kurz; Alessandra Palmigiano

doi:10.1093/logcom/exu064

Multi-type display calculus for propositional dynamic logic

G. Greco, Sabine Frittella, Alexander Kurz, Alessandra Palmigiano

Research output: Contribution to journal › Article › Academic › peer-review

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.

Original language	English
Pages (from-to)	2067-2104
Journal	Journal of Logic and Computation
Volume	26
Issue number	6
DOIs	https://doi.org/10.1093/logcom/exu064
Publication status	Published - 2016

Keywords

display calculus
propositional dynamic logic
multi-type proof- system

Access to Document

10.1093/logcom/exu064

Cite this

@article{9bcd9bde89c945ea8bb707c8dbb03d17,

title = "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.",

keywords = "display calculus, propositional dynamic logic, multi-type proof- system",

author = "G. Greco and Sabine Frittella and Alexander Kurz and Alessandra Palmigiano",

year = "2016",

doi = "10.1093/logcom/exu064",

language = "English",

volume = "26",

pages = "2067--2104",

journal = "Journal of Logic and Computation",

issn = "0955-792X",

publisher = "Oxford University Press",

number = "6",

}

TY - JOUR

T1 - Multi-type display calculus for propositional dynamic logic

AU - Greco, G.

AU - Frittella, Sabine

AU - Kurz, Alexander

AU - Palmigiano, Alessandra

PY - 2016

Y1 - 2016

N2 - 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.

AB - 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.

KW - display calculus

KW - propositional dynamic logic

KW - multi-type proof- system

U2 - 10.1093/logcom/exu064

DO - 10.1093/logcom/exu064

M3 - Article

SN - 0955-792X

VL - 26

SP - 2067

EP - 2104

JO - Journal of Logic and Computation

JF - Journal of Logic and Computation

IS - 6

ER -

Multi-type display calculus for propositional dynamic logic

Abstract

Keywords

Access to Document

Fingerprint

Cite this