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

• Autorzy: Balbiani P.
• Języki publikacji: EN

Abstrakty

EN

We devote this paper to the completeness of an axiom system for PDL - 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 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 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.

Słowa kluczowe

EN

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

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2003
• Tom: Vol. 56, nr 3
• Strony: 211--242
• Opis fizyczny: bibliogr. 25 poz.

Twórcy

autor

Balbiani P.

• Institut de Recherche en Informatique de Tuluse, Université Paul Sabatier, 118 rute de Narbonne, 31062 Toulouse Cedex 4, France,

Bibliografia

• [1] Balbiani, P.: A new proof of completeness for a relative modal logic with composition and intersection. Journal of Applied Non-Classical Logics 11 (2001) 269-280.
• [2] Balbiani, P., Farinas del Cerro, L.: Complete axiomatization of a relative modal logic with composition and intersection. Journal of Applied Non-Classical Logics 8 (1998) 325-335.
• [3] Balbiani, P., Vakarelov, D.: Iteration-free P D L with intersection: a complete axiomatization. Fundamenta Informaticæ45 (2001) 173-194.
• [4] Balbiani, P., Vakarelov, D.: P D L with intersection of programs: a complete axiomatization. Journal of Applied Non-Classical Logics, to appear.
• [5] Benanav, D., Kapur, D., Narendran, P.: Complexity of matching problems. In Jouannaud, J.-P. (Editor): Rewriting Techniques and Applications. Springer-Verlag, Lecture Notes in Computer Science 202 (1985) 417-429.
• [6] Blackburn, P., de Rijke, M., Venema, Y. Modal Logic. Cambridge University Press, Cambridge Tracts in Theoretical Computer Science 53 (2001).
• [7] Chagrov, A., Zakharyaschev, M. Modal Logic. Oxford University Press, Oxford Logic Guides 35 (1997).
• [8] Danecki, R.: Non-deterministic propositional dynamic logic is decidable. In Skowron, A. (Editor): Computation Theory. Springer-Verlag, Lecture Notes in Computer Science 208 (1985) 34-53.
• [9] Fisher, M., Ladner, R.: Propositional dynamic logic of regular programs. Journal of Computer and System Sciences 18 (1979) 194-211.
• [10] Gargov, G., Passy, S. A note on Boolean modal logic. In Petkov, P. (Editor): Mathematical Logic. Plenum Press (1990) 299-309.
• [11] Gargov, G., Passy, S., Tinchev, T. Modal environment for Boolean speculations In Skordev, D. (Editor): Mathematical Logic and its Applications. Plenum Press (1987) 253-263.
• [12] Goldblatt, R.: Axiomatising the Logic of Computer Programming. Springer-Verlag, Lecture Notes in Computer Science 130 (1982).
• [13] Harel, D.: First-Order Dynamic Logic. Springer-Verlag, Lecture Notes in Computer Science 68 (1979).
• [14] Harel, D.: Recurring dominoes: making the highly undecidable highly understandable. In Karpinski, M. (Editor): Foundations of Computation Theory. Springer-Verlag, Lecture Notes in Computer Science 158 (1983) 177-194.
• [15] Harel, D.: Dynamic logic. In Gabbay, D., Guenthner, F. (Editors): Handbook of Philosophical Logic, Volume II, Extensions of Classical Logic. Kluwer Academic Publishers, Synthese Library 165 (1984) 497-604.
• [16] Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press (2000).
• [17] Hughes, G., Cresswell, M.: A Companion to Modal Logic. Methuen (1984).
• [18] Kozen, D., Parikh, R.: An elementary proof of the completeness of P D L Theoretical Computer Science 14 (1981) 113-118.
• [19] Kozen, D., Tiuryn, J.: Logics of programs. In van Leeuwen, J. (Editor): Handbook of Theoretical Computer Science, Volume B, Formal Models and Semantics. Elsevier (1990) 789-840.
• [20] Lemmon, E., Scott, D.: The “Lemmon Notes”: an Introduction to Modal Logic. Blackwell (1977).
• [21] Marx, M., Venema, Y.: Multi-Dimensional Modal Logic. Kluwer Academic Publishers, Applied Logic Series 4 (1997).
• [22] Parikh, R.: Propositional dynamic logics of programs: a survey. In Engeler, E. (Editor): Logic of Programs. Springer-Verlag, Lecture Notes in Computer Science 125 (1981) 102-144.
• [23] Passy, S., Tinchev, T.: An essay in combinatory dynamic logic. Information and Computation 93 (1991) 263-332.
• [24] Pratt, V.: A near-optimal method for reasoning about action. Journal of Computer and System Sciences 20 (1980) 231-254.
• [25] Segerberg, K.: A completeness theorem in the modal logic of programs. In Traczyk, T. (Editor): Universal Algebra and Applications. Polish Scientific Publishers, Banach Center Publications 9 (1982) 31-36.