Abstract

This note presents a point of view upon the notions of programsubstitution which are the tools for proving properties of programs of algorithmic logics [5], [3] being sufficiently strong and universal to comprise almost all previously introduced theories of programming, and the so-called extended algorithmic logic [1], [2] and algorithmic logic with nondeterministic programs [4]. It appears that the mentioned substitution rule allows us to examine more deeply algorithmic properties of terms, formulas and programs. Besides the problem of Post-completeness and structural completeness of algorithmic logics strengthened additionally by the rule of substitution is raised