Decision procedure for checking validity of PAL formulas

  • Igor Walukiewicz
Part III Communications
Part of the Lecture Notes in Computer Science book series (LNCS, volume 464)


The aim of propositional algorithmic logic (PAL) is to investigate properties of simple nondeterministic while-program schemes on propositional level. We present algorithm for checking validity of PAL sequents based on a finite Gentzen-type axiomatization, which reaches lower complexity limit. Additionally we obtain small model theorem for PAL.


Decision Procedure Current Node Propositional Variable Check Validity Canonical Structure 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Chlebus, On the Decidability of Propositional Algorithmic Logic, Zeitschr. f. math. Logik 28, 247–261 (1982)Google Scholar
  2. 2.
    Fisher M. J. and Ladner R. E., Propositional dynamic logic of regular programs, J. Comput. Syst. Sci. 18 194–211.Google Scholar
  3. 3.
    Harel D., Dynamic Logic, Handbook of Philosophical Logic Vol 11, 197–604 (1984)Google Scholar
  4. 4.
    Mirkowska G., PAL — propositional algorithmic logic, Fund Informaticae 4, 675–760. Also in Lecture Notes in Computer Science, Vol 125, Springer-Verlag pp.23–101 (1981)Google Scholar
  5. 5.
    Nishimura H., Sequential Method in Propositional Dynamic Logic, Acta Informatica 12, pp. 377–400 (1979)Google Scholar
  6. 6.
    Nishimura H., Semantical Analysis of Constructive PDL, Publ. Res. Inst. Math. Sci. Kyoto Univ. (1981)Google Scholar
  7. 7.
    Salwicki A., Formalized algorithmic languages, Bull. Acad. Polon Sci. Ser Sci. Math. Astron. Phys. 18, pp. 227–232 (1970)Google Scholar
  8. 8.
    Street R.S., Propositional dynamic logic of looping and converse is elementary decidable, Inf. and Control 54 pp. 121–141. (1982)Google Scholar
  9. 9.
    Walukiewicz I. Gentzen Type Axiomatization of PAL to appear in Proceedings of MFCS 90, Springer-Verlag.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1990

Authors and Affiliations

  • Igor Walukiewicz
    • 1
  1. 1.Institute of InformaticsWarsaw UniversityWarszawaPoland

Personalised recommendations