A Non-wellfounded, Labelled Proof System for Propositional Dynamic Logic

Simon Docherty; Reuben Rowe

doi:10.1007/978-3-030-29026-9_19

A Non-wellfounded, Labelled Proof System for Propositional Dynamic Logic

Simon Docherty, Reuben Rowe

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

94 Downloads (Pure)

Abstract

We define an infinitary labelled sequent calculus for PDL, 퐆3퐏퐃퐋∞. A finitarily representable cyclic system, 퐆3퐏퐃퐋휔, is then given. We show that both are sound and complete with respect to standard models of PDL and, further, that 퐆3퐏퐃퐋∞ is cut-free complete. We additionally investigate proof-search strategies in the cyclic system for the fragment of PDL without tests.

Original language	English
Title of host publication	TABLEAUX 2019
Subtitle of host publication	Automated Reasoning with Analytic Tableaux and Related Methods
Publisher	Springer
Pages	335-352
Number of pages	18
ISBN (Electronic)	978-3-030-29026-9
ISBN (Print)	978-3-030-29025-2
DOIs	https://doi.org/10.1007/978-3-030-29026-9_19
Publication status	E-pub ahead of print - 14 Aug 2019

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	11714

Access to Document

10.1007/978-3-030-29026-9_19

Accepted ManuscriptAccepted author manuscript, 420 KB

Cite this

@inproceedings{28588ade282a4e04b5c7f7410931575d,

title = "A Non-wellfounded, Labelled Proof System for Propositional Dynamic Logic",

abstract = "We define an infinitary labelled sequent calculus for PDL, 퐆3퐏퐃퐋∞. A finitarily representable cyclic system, 퐆3퐏퐃퐋휔, is then given. We show that both are sound and complete with respect to standard models of PDL and, further, that 퐆3퐏퐃퐋∞ is cut-free complete. We additionally investigate proof-search strategies in the cyclic system for the fragment of PDL without tests.",

author = "Simon Docherty and Reuben Rowe",

year = "2019",

month = aug,

day = "14",

doi = "10.1007/978-3-030-29026-9_19",

language = "English",

isbn = "978-3-030-29025-2",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "335--352",

booktitle = "TABLEAUX 2019",

}

TY - GEN

T1 - A Non-wellfounded, Labelled Proof System for Propositional Dynamic Logic

AU - Docherty, Simon

AU - Rowe, Reuben

PY - 2019/8/14

Y1 - 2019/8/14

N2 - We define an infinitary labelled sequent calculus for PDL, 퐆3퐏퐃퐋∞. A finitarily representable cyclic system, 퐆3퐏퐃퐋휔, is then given. We show that both are sound and complete with respect to standard models of PDL and, further, that 퐆3퐏퐃퐋∞ is cut-free complete. We additionally investigate proof-search strategies in the cyclic system for the fragment of PDL without tests.

AB - We define an infinitary labelled sequent calculus for PDL, 퐆3퐏퐃퐋∞. A finitarily representable cyclic system, 퐆3퐏퐃퐋휔, is then given. We show that both are sound and complete with respect to standard models of PDL and, further, that 퐆3퐏퐃퐋∞ is cut-free complete. We additionally investigate proof-search strategies in the cyclic system for the fragment of PDL without tests.

U2 - 10.1007/978-3-030-29026-9_19

DO - 10.1007/978-3-030-29026-9_19

M3 - Conference contribution

SN - 978-3-030-29025-2

T3 - Lecture Notes in Computer Science

SP - 335

EP - 352

BT - TABLEAUX 2019

PB - Springer

ER -