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 proceeding › Conference contribution
E-pub ahead of print
Documents
- Accepted Manuscript
Accepted author manuscript, 420 KB, PDF document
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 | |
| Publication status | E-pub ahead of print - 14 Aug 2019 |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Publisher | Springer |
| Volume | 11714 |
This open access research output is licenced under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.
ID: 34707934