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



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 languageEnglish
Title of host publicationTABLEAUX 2019
Subtitle of host publicationAutomated Reasoning with Analytic Tableaux and Related Methods
Number of pages18
ISBN (Electronic)978-3-030-29026-9
ISBN (Print)978-3-030-29025-2
Publication statusE-pub ahead of print - 14 Aug 2019

Publication series

NameLecture Notes in Computer Science
This open access research output is licenced under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.

ID: 34707934