Abstract
The aim of propositional algorithmic logic is to investigate the properties of program connectives. Complete axiomatic systems for deterministic as well as for nondeterministic interpretations of program variables are presented. They constitute basic sets of tools useful in the practice of proving the properties of program schemes. Propositional theories of data structures, e.g. the arithmetic of natural numbers and stacks, are constructed. This shows that in many aspects PAL is close to first-order algorithmic logic. Tautologies of PAL become tautologies of algorithmic logic after replacing program variables by programs and propositional variables by formulas. Another corollary to the completeness theorem asserts that it is possible to eliminate nondeterministic program variables and replace them by schemes with deterministic atoms.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Andreka H.,Nemeti I., Completeness of Floyd logic, Bulletin of section of logic, vol. 7 (1978)
Andreka H.,Nemeti I.,Sain I., Completeness problem in verification of programs and program schemes. Proc.MFCS 79 J.Becvar ed. in Lecture Notes on Computer Science vo.74
Banachowski L.,Kreczmar A.,Mirkowska G.,Rasiowa H.,Salwicki A., An introduction to algorithmic logic. Metamathematical investigations in the theory of programs, in Banach Center Publications vol.2 Mathematical Foundations of Computer Science (1977)
Berman F., A completeness technique for D-axiomatizable semantics, Proc.11th Ann.ACM Symp.on Thery of Computing Atlanta, Georgia May 1979
Chlebus B., On decidability of propositional algorithmic logic, Institute of Informatics Reports, University of Warsaw, 1979
Constable R., On the theory of programming logics, Proc. 9th Ann.ACM Symp. on Theory of Computing Boulder.Col. May 1977, pp. 269–285
Dahn B., Generalized Kripke-Models, Bull.de l'Akademie Polonaise des Sci.Ser.Math. vol.XXI No 12(1973), pp. 1073–1077
Engeler E., Algorithmic properties of structures, Math.Systems Theory 1 (1967), pp. 183–195
Floyd R.W., Assigning Meanings to Programs, in Mathematical Aspects of Computer Science ed. J.T.Schwartz, 1967, pp.19–32
Fisher M.J.,Ladner R.E., Propositional modal logic of programs, Proc. 9th Ann.ACM Symp. on Theory of Computing. Boulder.Col., May 1977, pp.286–294
Grabowski M., The set of tautologies of zero-order algorithmic logic is decidable, Bull.Acad.Pol.Sci.Ser.Math. No 20 (1972) pp.575–582
Harel D.,Pratt V., Nondeterminism in logic of programs, Proc. 9th Ann.ACM Symp. on Theory of Computing, Boulder.Colorado, May 1977, pp.261–268
Hoare C.A., An axiomatic basis for computer programming, CACM 12, (1969), pp.576–580
Kozen D., A representation theorem for models of-free PDL, Report RC 7864, IBM Research, Yorktown Heights, New York, 1979
Kozen D., On the representation of dynamic algebras, Report RC 7898, IBM Research, Yorktown Heights, New York, 1979
Mirkowska G., On formalized systems of algorithmic logic, Bull. Acad.Pol.Sci.Ser.Math. 18 (1970) pp.499–505
Mirkowska G., Algorithmic logic with nondeterministic programs, Fundamenta Informaticae
Mirkowska G., Multimodal logic, Technical report, University of Warszaw 1979
Mirkowska G., On algorithmic algebras, manuscript 1980
Mirkowska G., On propositional algorithmic theory related to arithmetic, manuscript 1980
Muldner T., Salwicki A., On algorithmic properties of concurent programs, manuscript 1979
Parikh R., A completeness result for PDL, Proc. MFCS '78, Lecture Notes in Computer Science, vol. 64, pp.403–416
Pratt V., Semantical Considerations of Floyd-Hoare logic, 17th IEEE Symposium on Foundations of Computer Science (1976), 109–121
Pratt V., Models of program logics, 20th IEEE Conference on Foundations of Computer Science, San Juan, PR,Oct.1979
Pratt V., Dynamic algebras and the nature of induction, preprint MIT /LCS/ TM-159, March 1980
Rasiowa H., Sikorski R., Mathematics of Metamathematics, PWN Warszaw 1963
Salwicki A., On algorithmic theory of stacks, ICS PAS report No 337, to appear in Fundamenta Informaticae
Salwicki A., Formalized algorithmic languages, Bull.Acad.Pol. Sci.,Ser.Math. vol.18 No5, (1970), pp. 227–232
Segerberg K., A completeness theorem in the modal logic of programs, Notices of the AMS, 24,6, A-552, (1977)
Yanov J., On equivalence of operator schemes, Problems of Cybernetic 1, (1959), pp.1–100.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1981 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mirkowska, G. (1981). PAL — Propositional algorithmic logic. In: Engeler, E. (eds) Logic of Programs. Logic of Programs 1979. Lecture Notes in Computer Science, vol 125. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-11160-3_3
Download citation
DOI: https://doi.org/10.1007/3-540-11160-3_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-11160-3
Online ISBN: 978-3-540-38631-5
eBook Packages: Springer Book Archive