Interpolation for Converse PDL
| Authors |
|
|---|---|
| Publication date | 2026 |
| Host editors |
|
| Book title | Automated Reasoning with Analytic Tableaux and Related Methods |
| Book subtitle | 34th International Conference, TABLEAUX 2025, Reykjavik, Iceland, September 27–29, 2025 : proceedings |
| ISBN |
|
| ISBN (electronic) |
|
| Series | Lecture Notes in Computer Science |
| Event | 34th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2025 |
| Pages (from-to) | 258–277 |
| Number of pages | 20 |
| Publisher | Cham: Springer |
| Organisations |
|
| Abstract |
Converse PDL is the extension of propositional dynamic logic with a converse operation on programs. Our main result states that Converse PDL enjoys the (local) Craig Interpolation Property, with respect to both atomic programs and propositional variables. As a corollary we establish the Beth Definability Property for the logic.
Our interpolation proof is based on an adaptation of Maehara’s proof-theoretic method. For this purpose we introduce a sound and complete cyclic sequent system for this logic. This calculus features an analytic cut rule and uses a focus mechanism for recognising successful cycles. |
| Document type | Conference contribution |
| Language | English |
| Published at |
https://doi.org/10.48550/arXiv.2508.21485
(Accepted author manuscript)
https://doi.org/10.1007/978-3-032-06085-3_14
(Final published version)
|
| Downloads |
978-3-032-06085-3_14
(Final published version)
|
| Permalink to this page | |