Algorithmic logic and its applications in the theory of programs I

Article type: Research Article

Authors: Mirkowska, Grażyna^a

Affiliations: [a] University of Warsaw

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.

DOI: 10.3233/FI-1977-1102

Journal: Fundamenta Informaticae, vol. 1, no. 1, pp. 1-17, 1977