Abstract
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.
Get full access to this article
View all access options for this article.