Algorithmic logic and its applications in the theory of programs I

The paper presents tools for formalizing and proving properties of programs. The language of algorithmic logic constitutes an extension of a programming language by formulas that describe algorithmic properties. The paper contains two axiomatizations of algorithmic logic, which are complete. It can be proved that every valid algorithmic property possesses a formal proof. An analogue of Herbrand theorem and a theorem on the normal form of a program are proved. Results of meta-mathematical character are applied to theory of programs, e.g. Paterson’s theorem is an immediate corollary to Herbrand’s theorem.