**A Non-wellfounded, Labelled Proof System for Propositional Dynamic Logic.** / Docherty, Simon; Rowe, Reuben.

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

E-pub ahead of print

**A Non-wellfounded, Labelled Proof System for Propositional Dynamic Logic.** / Docherty, Simon; Rowe, Reuben.

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

Docherty, S & Rowe, R 2019, A Non-wellfounded, Labelled Proof System for Propositional Dynamic Logic. in *TABLEAUX 2019: Automated Reasoning with Analytic Tableaux and Related Methods.* Lecture Notes in Computer Science, vol. 11714, Springer, pp. 335-352. https://doi.org/10.1007/978-3-030-29026-9_19

Docherty, S., & Rowe, R. (2019). A Non-wellfounded, Labelled Proof System for Propositional Dynamic Logic. In *TABLEAUX 2019: Automated Reasoning with Analytic Tableaux and Related Methods *(pp. 335-352). (Lecture Notes in Computer Science; Vol. 11714). Springer. https://doi.org/10.1007/978-3-030-29026-9_19

Docherty S, Rowe R. A Non-wellfounded, Labelled Proof System for Propositional Dynamic Logic. In TABLEAUX 2019: Automated Reasoning with Analytic Tableaux and Related Methods. Springer. 2019. p. 335-352. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-030-29026-9_19

@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 -