Extension of PDL and consequence relations

  • Slavian Radev
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 208)


Most of the deduction algorithms are of the form of regular expressions. To investigate some properties of these deductions we introduce an extension of PDL with propositional constants and infinite conjunctions and disjunctions. We treat the formulas of the object logical language for which the deductions are as propositional variables, the sets of formulas — as propositional constants and the deductions — as regular programs. A Hilbert's style axiomatization of this logic is shown to be complete for countable Kripke structures of sets of formulas.

Examples include a logic for the PDL logical consequences, a kind of a nonmonotonic deduction algorithm and some properties of logical consequences.


PDL infinitary logic logical consequence relations deduction methods artificial intelligence monotonicity 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [A]
    H. Andréka. Sharpening the Characterization of the Power of Floyd method, Lecture Notes in Computer Science 148 (1983) 1–26Google Scholar
  2. [B]
    J.Barwise. Admissible Sets and Structures, Springer-Verlag, 1975Google Scholar
  3. [Be]
    J.van Benthem. Partiality and Nonmonotonicity in Classical Logic, report ISLI, 1984Google Scholar
  4. [Bu]
    A. Bundy. The Computer Modelling of Mathematical Reasoning, Academic Press, 1983Google Scholar
  5. [FL]
    M. Fischer and R. Ladner. Propositional Dynamic Logic of Regular Programs, J. Comp. Sys. Sci. 18 (1979) 194–211Google Scholar
  6. [G]
    D.Gabbay. Investigations in Modal and Tense Logics with Applications to Problems in Philosophy and Linguistics, D.Reidel, 1976Google Scholar
  7. [GS]
    Y. Gurevich and S. Shelah. Interpreting Second-Order Logic in the Monadic Logic of Linear Order, J. Symbolic Logic, 48 (1983) 816–828Google Scholar
  8. [HPS]
    D. Harel, A. Pnueli and J. Stavi. Further Results on Propositional Dynamic Logic of Nonregular Programs, Lecture Notes in Computer Science 131 (1982) 124–136Google Scholar
  9. [K]
    J.Keisler. Model Theory for Infinitary Logic, North-Holland, 1971Google Scholar
  10. [Ko]
    D. Kozen. On Induction vs. ж-Continuity, Lecture Notes in Computer Science 131 (1982) 167–176Google Scholar
  11. [MP]
    Z. Manna and A. Pnueli. Verification of Concurrent Programs: Temporal Proof Principles, Lecture Notes in Computer Science 131 (1982) 200–252Google Scholar
  12. [M]
    D. Miller. Expansion Tree Proofs and their Conversion to Natural Deduction Proofs, Lecture Notes in Computer Science 170 (1984) 375–393Google Scholar
  13. [N]
    I. N'emeti. Nonstandard Dynamic Logic, Lecture Notes in Computer Science 131 (1982) 311–348Google Scholar
  14. [P]
    S.Passy. Combinatory PDL, Ph.D. Thesis, July 1984, SofiaGoogle Scholar
  15. [PT]
    S. Passy and T. Tinchev. PDL with Data Constants, Inf. Proc. Letters 20 (1985) 35–41Google Scholar
  16. [Pl]
    D. Plaisted. Using Examples, Case Analysis, and Dependency Graphs in Theorem Proving, Lecture Notes in Computer Science 170 (1984) 356–374Google Scholar
  17. [R1]
    S.Radev. Infinitary Propositional Normal Modal Logic and Programming Languages, Ph.D. Thesis, November 1981, WarsawGoogle Scholar
  18. [R2]
    S. Radev. Propositional Logics of Formal Languages, Fundamenta Informaticae VII 4 (1984)Google Scholar
  19. [S]
    P. Schroeder-Heister. A Natural Extension of Natural Deduction, J. Symbolic Logic, 49 (1984) 1284–1300Google Scholar
  20. [T]
    S. Thomason. Reduction of Second-Order Logic to Modal Logic, Zait. Math. Logic und Grund. Math. 21 (1975) 107–114Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1985

Authors and Affiliations

  • Slavian Radev
    • 1
  1. 1.Section of Mathematical LogicInstitute of Mathematics, BANSofiaBulgaria

Personalised recommendations