PAL – Propositional Algorithmic Logic

Article type: Research Article

Authors: Mirkowska, Grażyna

Affiliations: University of Warsaw, Institute of Mathematics

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.

Keywords: Logic of programs, algorithmic logic, nondeterminism, completeness

DOI: 10.3233/FI-1981-4310

Journal: Fundamenta Informaticae, vol. 4, no. 3, pp. 675-760, 1981