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

Article type: Research Article

Authors: Balbiani, Philippe

Affiliations: Institut de recherche en informatique de Toulouse, Université Paul Sabatier, 118 route de Narbonne, 31062 Toulouse Cedex 4, France

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}.

Keywords: propositional modal logic, propositional dynamic logic, composition of programs, intersection of programs, test on a formula, deductive completeness, subordination method

Journal: Fundamenta Informaticae, vol. 56, no. 3, pp. 211-242, 2003