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

TABLEAUX 2019: Automated Reasoning with Analytic Tableaux and Related Methods. Springer, 2019. p. 335-352 (Lecture Notes in Computer Science; Vol. 11714).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

E-pub ahead of print

Standard

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

TABLEAUX 2019: Automated Reasoning with Analytic Tableaux and Related Methods. Springer, 2019. p. 335-352 (Lecture Notes in Computer Science; Vol. 11714).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Harvard

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

APA

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

Vancouver

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

Author

Docherty, Simon ; Rowe, Reuben. / A Non-wellfounded, Labelled Proof System for Propositional Dynamic Logic. TABLEAUX 2019: Automated Reasoning with Analytic Tableaux and Related Methods. Springer, 2019. pp. 335-352 (Lecture Notes in Computer Science).

BibTeX

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

}

RIS

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 -