Eliminating Unorthodox Derivation Rules in an Axiom System for Iteration-free PDL with Intersection

Abstract

We devote this paper to the completeness of an axiom system for PDL^{∩}_{0} — a variant of PDL which includes the program operations of composition and intersection. Most of the difficulty in the proof of the completeness theorem for PDL^{∩}_{0} lies in the fact that intersection of accessibility relations is not modally definable. We overcome this difficulty by considering the concepts of theory and large program. Theories are sets of formulas that contain PDL^{∩}_{0} and are closed under the inference rule of modus ponens. Large programs are built up from program variables and theories by means of the operations of composition and intersection, just as programs are built up from program variables and tests. Adapting these concepts to the subordination method, we can prove the completeness of our deductive system for PDL^{∩}_{0}.