A Canonical Model Construction for Iteration-Free PDL with Intersection
Florian Bruse (University of Kassel), Daniel Kernberger (University of, Kassel), Martin Lange (University of Kassel)
TL;DR
This paper develops a normal form and a canonical model construction for the iteration-free fragment of Propositional Dynamic Logic with Intersection and Tests, leading to a complete axiom system.
Contribution
It introduces a normal form and a refined canonical model for the complex logic, establishing strong completeness for the axiom system.
Findings
Normal form minimizes operator interaction
Refined canonical model construction
Strong completeness proof for the axiom system
Abstract
We study the axiomatisability of the iteration-free fragment of Propositional Dynamic Logic with Intersection and Tests. The combination of program composition, intersection and tests makes its proof-theory rather difficult. We develop a normal form for formulae which minimises the interaction between these operators, as well as a refined canonical model construction. From these we derive an axiom system and a proof of its strong completeness.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.