Algorithmic Logic: Różnice pomiędzy wersjami
(→Bibliography) |
(→Bibliography) |
||
Linia 8: | Linia 8: | ||
In 1969 the program of research was formulated in the Ph.D. thesis of A. Salwicki. | In 1969 the program of research was formulated in the Ph.D. thesis of A. Salwicki. | ||
== Bibliography == | == Bibliography == | ||
− | # [Mirkowska, Salwicki 1987] {{Cytuj | + | # [Mirkowska, Salwicki 1987] {{Cytuj książkę | odn=tak | nazwisko=Mirkowska |imię= Grażyna | tytuł = Algorithmic Logic | nazwisko2= Salwicki |imię2=Andrzej | wydawca =PWN & D.Reidel | miejsce= Warszawa & Dordrecht | strony= 374 }} |
# [Kreczmar 1977a] {{Cytuj pismo |odn=tak |odn=a | nazwisko = Kreczmar | imię = Antoni | tytuł = Effectivity problems of Algorithmic Logic | czasopismo = Fundamenta Informaticae | rok = 1977}} | # [Kreczmar 1977a] {{Cytuj pismo |odn=tak |odn=a | nazwisko = Kreczmar | imię = Antoni | tytuł = Effectivity problems of Algorithmic Logic | czasopismo = Fundamenta Informaticae | rok = 1977}} | ||
# [Kreczmar 1977b] {{Cytuj pismo| odn=tak |odn=b | imię=Antoni | nazwisko=Kreczmar |tytuł=Programmability in Fields |czasopismo=Fundamenta Informaticae |strony=195-230 |rok=1977}} | # [Kreczmar 1977b] {{Cytuj pismo| odn=tak |odn=b | imię=Antoni | nazwisko=Kreczmar |tytuł=Programmability in Fields |czasopismo=Fundamenta Informaticae |strony=195-230 |rok=1977}} |
Wersja z 18:10, 12 kwi 2014
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 origins of algorithmic logic go to papers of Yanov, H. Thiele, Erwin Engeler. In 1969 the program of research was formulated in the Ph.D. thesis of A. Salwicki.
Bibliography
- [Mirkowska, Salwicki 1987] Grażyna Mirkowska, Andrzej Salwicki: Algorithmic Logic. Warszawa & Dordrecht: PWN & D.Reidel, s. 374.
- [Kreczmar 1977a] Antoni Kreczmar. Effectivity problems of Algorithmic Logic. „Fundamenta Informaticae”, 1977.
- [Kreczmar 1977b] Antoni Kreczmar. Programmability in Fields. „Fundamenta Informaticae”, s. 195-230, 1977.
- [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.
- [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.