Multi-type display calculus for propositional dynamic logic

Sabine Frittella; Giuseppe Greco; Alexander Kurz; Alessandra Palmigiano

doi:10.1093/logcom/exu064

Multi-type display calculus for propositional dynamic logic

Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano

Ethics & Philosophy of Technology

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

23 Citations (Scopus)

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
Number of pages	38
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
Multi-type proof-system
Propositional dynamic logic

Access to Document

10.1093/logcom/exu064

Cite this

@article{686b238e35b14394a2e8aecab9c8f522,

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, Multi-type proof-system, Propositional dynamic logic",

author = "Sabine Frittella and Giuseppe Greco 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 - Frittella, Sabine

AU - Greco, Giuseppe

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 - Multi-type proof-system

KW - Propositional dynamic logic

UR - http://www.scopus.com/inward/record.url?scp=85014713948&partnerID=8YFLogxK

U2 - 10.1093/logcom/exu064

DO - 10.1093/logcom/exu064

M3 - Article

AN - SCOPUS:85014713948

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

Other files and links

Fingerprint

Cite this