Algorithmic Logic: Różnice pomiędzy wersjami

Wersja z 20:28, 28 lis 2014

This page is under construction

Algorithmic logic is a calculus in which one can express the semantical properties of programs and it allows to construct proofs of the formulas. In this way one can prove property like correctness by proving the corresponding formula that express the property.

Structure of AL

An algorithmic logic is a pair [math]\mathcal{AL} = \langle \mathcal{L}, \mathcal{C} \rangle [/math], where [math]\mathcal{L} [/math] is a formalized language of algorithmic logic and [math]\mathcal{C} [/math] is i a logical consequence operation defined by the notions of logical axioms, inference rules and the notion of (formal) proof. An algorithmic language [math]\mathcal{L} [/math] is a pair consisting of the alphabet of [math]\mathcal{L} [/math] and the set of weel-formed expressions, [math]\mathcal{L} = \langle A, WFF \rangle [/math], where [math] A [/math] is the alphabet, i.e. the set of admissible symbols and [math] WFF [/math] is the set of well formed expressions of the language.

History

The first papers on properties of programs appeared in the 50-ies of XX century. To mention a few: Yanov, Sh. Igarashi. Later the papers of Helmut Thiele and of Erwin Engeler are important ones.

In 1969 the program of research of algorithmic logic was formulated in the Ph.D. thesis of A. Salwicki.

pre algorithmic logic

Paper of R.W. Floyd brought some light on proving programs correct. Later C.A.R. Hoare proposed another formalization based on the ideas of Floyd. S. Cook addressed the problem of completeness of Floyd-Hoare calculus and formulated the so called relative completeness theorem.

In the light of the paper [Goraj, Mirkowska, Paluszkiewicz ↓] this theorem is unnecessary. Theorem 5 of this paper states that notion of feasible and of acceptable desciption of program coincide. In other words if a verification condition of a program is valid in all models of a theory then it is provable from the axioms of the theory.

Bibliography

1. [Mirkowska, Salwicki 1987] Grażyna Mirkowska, Andrzej Salwicki: Algorithmic Logic. Warszawa & Dordrecht: PWN & D.Reidel, s. 374.
2. [AL4software] Grażyna Mirkowska, Andrzej Salwicki: Algorithmic Logic for Software Construction and Verification. Dąbrowa Leśna: Dąbrowa Research, 2014, s. 154.
3. [Kreczmar 1977a] Antoni Kreczmar. Effectivity problems of Algorithmic Logic. „Fundamenta Informaticae”, 1977. 
4. [Kreczmar 1977b] Antoni Kreczmar. Programmability in Fields. „Fundamenta Informaticae”, s. 195-230, 1977. 
5. [Kreczmar 1979] Antoni Kreczmar: Some historical remarks on algorithmic logic. T. Algorithms in Modern Mathematics and Computer Science. Berlin: Springer Vlg, 1979, s. 999-1000, seria: LNCS. ISBN 0123456789.
6. [Banachowski i in.] Lech Banachowski, Antoni Kreczmar, Grażyna Mirkowska, Helena Rasiowa, Andrzej Salwicki: An introduction to Algorithmic Logic - Metamathematical Investigations of Theory of Programs. T. 2: Banach Center Publications. Warszawa: PWN, 1977, s. 7-99, seria: Banach Center Publications. ISBN 123. [1]
7. [Goraj, Mirkowska, Paluszkiewicz] Anna Goraj, Grażyna Mirkowska, Anna Paluszkiewicz. On the notion of the description of the program. „Bull. Pol. Acad. Sci. Ser. Astr. Math. Phys.”, s. 499-505, 1970. 
8. [Yanov 1959] Yuri I. Yanov. The Logical schemes in Algorithms. „Problems of Cybernetics”, s. 82-140, 1959. 
9. [Engeler 1967 ] Erwin Engeler. Algorithmic properties of Structures. „Math. System Theory”, s. 183-195, 1967.