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

Simon Docherty, Reuben Rowe

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

82 Downloads (Pure)


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

Cite this