Iteration-free PDL with Intersection: a Complete Axiomatization

Article type: Research Article

Authors: Balbiani, Philippe | Vakarelov, Dimiter

Abstract: This paper is devoted to the completeness issue of PDL_0^∩ – an iteration-free fragment of Propositional Dynamic Logic with intersection of programs. The trouble with PDL_0^∩ is that the operation of intersection is not modally definable. Using new techniques connected with rules for intersection and the notions of large and maximal programs, the paper demonstrates that the presented proof theory for PDL_0^∩ is complete for the standard Kripke semantics of PDL_0^∩.

Keywords: PDL with intersection, modal rules for intersection, maximal programs

Journal: Fundamenta Informaticae, vol. 45, no. 3, pp. 173-194, 2001