2025/08/29 by Johannes Kloibhofer, Kloibhofer, Johannes, Valentina Trucco Dalmas +3
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · doi:10.48550/arxiv.2508.21485
openalex publication_date 2025/08/29 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.