A Canonical Model Construction for Iteration-Free PDL with Intersection

2016/09/13 by Florian Bruse, Daniel Kernberger, Martin Lange
Computer Science · Mathematics · #Algebra over a field #Algorithm #Axiom #Completeness (order theory) #Discrete mathematics #Formal Methods in Verification #Fragment (logic) #Intersection (aeronautics) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Mathematics #Propositional calculus #Pure mathematics #cs.LO

paper · pdf · doi:10.4204/eptcs.226.9

published as EPTCS 226, 2016, pp. 120-134 · In Proceedings GandALF 2016, arXiv:1609.03648

openalex publication_date 2016/09/13 · arxiv created 2016/09/14 · arxiv updated 2016/09/15 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/06

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.

Citations

• Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification
• A near-optimal method for reasoning about action
• Propositional dynamic logic of regular programs