Algorithmic Logic - Historia wersji

AndrzejSalwicki: /* Algorithmic theories */

2024-11-11T14:19:54Z

‎Algorithmic theories

AndrzejSalwicki o 14:17, 11 lis 2024

2024-11-11T14:17:53Z

AndrzejSalwicki: /* Algorithmic theories */

2024-11-11T14:15:33Z

‎Algorithmic theories

AndrzejSalwicki o 12:29, 11 lis 2024

2024-11-11T12:29:42Z

AndrzejSalwicki o 12:19, 11 lis 2024

2024-11-11T12:19:32Z

AndrzejSalwicki: /* Introduction */

2018-02-03T09:00:55Z

‎Introduction

AndrzejSalwicki: /* Other logics of programs */

2017-08-08T16:49:15Z

‎Other logics of programs

AndrzejSalwicki: /* Floyd-Hoare logic */

2017-08-08T16:48:43Z

‎Floyd-Hoare logic

AndrzejSalwicki: /* Algorithmic theories */

2017-08-08T16:35:16Z

‎Algorithmic theories

AndrzejSalwicki: /* Algorithmic theories */

2017-08-08T16:30:22Z

‎Algorithmic theories

@@ Linia 46: / Linia 46: @@
 Here we shall collect axiomatizations of various algorithmic theories. Each set <math>S</math> of this collection may be conceived as specification of a class <math>C</math>  that implements the set  <math>S</math>.<br />
-[[Algorithmic theory of natural numbers <math>\mathcal{ATN} </math> ]]<br />
+[[Algorithmic theory of natural numbers  ]]<br />
 [[Algorithmic theory of integers]]<br />
 [[Algorithmic theory of rational numbers]]<br />

@@ Linia 46: / Linia 46: @@
 Here we shall collect axiomatizations of various algorithmic theories. Each set <math>S</math> of this collection may be conceived as specification of a class <math>C</math>  that implements the set  <math>S</math>.<br />
-[[Algorithmic theory of natural numbers<math>\mathcal{ATN} </math> ]]<br />
+[[Algorithmic theory of natural numbers <math>\mathcal{ATN} </math> ]]<br />
 [[Algorithmic theory of integers]]<br />
 [[Algorithmic theory of rational numbers]]<br />

@@ Linia 46: / Linia 46: @@
 Here we shall collect axiomatizations of various algorithmic theories. Each set <math>S</math> of this collection may be conceived as specification of a class <math>C</math>  that implements the set  <math>S</math>.<br />
-[[Algorithmic theory of natural numbers]]<br />
+[[Algorithmic theory of natural numbers<math>\mathcal{ATN} </math> ]]<br />
 [[Algorithmic theory of integers]]<br />
 [[Algorithmic theory of rational numbers]]<br />

@@ Linia 18: / Linia 18: @@
 Figure  5 should be self explanatory. It remains to decide what to do when a computation of program K does not bring a result . It may happen that computation of program K is infinite or another error occurred.   In such case it is impossible to assert that ''for  data v the computation of program K ends successfully and the results satisfy the condition '' <math>\alpha</math>'. Hence in this case the value of formula   <math>K\alpha</math> is '''false'''..<br />
 O logice algorytmicznej możemy też powiedzieć, że jest [[rachunek programów|''rachunkiem programów'']].   Język logiki algorytmicznej zawiera programy i formuły algorytmiczne. Ważne jest to, że każda semantyczna własność programów np. poprawność, równowazność, kończenie obliczeń lub przeciwnie zapętlanie, ... może być wyrażona przez odpowiednią formułę. Pozwala to zamienić zadanie wykazania, że pewien program  <math>P</math> posiada pewną własnośc semantyczną <math>S</math> na zadanie udowodnić formułę <math>\beta</math> należąca do języka logiki algorytmicznej. <br />'''Przykład''' <br />
 Własność: ''Dla każdych danych <math>v</math>, jeśli  program <math>K</math> rozpoczyna obliczenia z danymi spełniającymi warunek <math>\alpha</math> to jego obliczenie zakończy się (nie będzie zapętlenia, ani przerwania obliczeń) i jego wyniki spełniają warunek <math>\beta</math>'', jest wyrażana formułą <math>\alpha \rightarrow K\beta</math>. Nie musimy więc podejmować trudu testowania czy dla kazdych danych obliczenie programu K będzie skończone i ... <br />

@@ Linia 5: / Linia 5: @@
 == Introduction ==
-Algorithmic logic is a calculus of logic. It is an attractive workplace for software engineers as well as for mathematically oriented people. It is quite reasonable to give it another name ''calculus of programs''.
+Algorithmic logic is a calculus of logic, moreover it is also a calculus of programs. It is an attractive workplace for software engineers as well as for mathematically oriented people. It is quite reasonable to give it another name ''calculus of programs''.
 [[Plik:4logiki.jpg|thumb|center |750px| Fig. 1  Four logical systems and their sets of well formed expressions ]]
 Figure 1 shows relations among four logical calculi. An arrow     <math>\mathcal{L}\rightarrow\mathcal{L}'</math> between two logical calculi <math>\mathcal{L}</math> and <math>\mathcal{L}'</math> has following meaning: ''Every tautology'' <math>\alpha</math> ''of calculus'' <math>\mathcal{L}</math> ''becmes a tatutology of calculus ''<math>\mathcal{L}</math>' ''when atoms of formula '' <math>\alpha</math> '' are replaced by formulas of calculus'' <math>\mathcal{L}</math>. More insight can be gained by comparison of sets of well formed formulas  <math>\mathcal{WFF} </math>.  <br />

@@ Linia 71: / Linia 71: @@
 == Other logics of programs ==
-You may ask how calculus of programs is related to other calculi: e.g. Floyd, Hoare, Dijkstra, dynamic logic, etc.?
+You may ask how calculus of programs is related to other calculi: e.g. Floyd, Hoare, Dijkstra, dynamic logic, etc.?<br />
 [[calculus of Floyd]]<br />
 [[logic of Hoare]]<br />

@@ Linia 70: / Linia 70: @@
 In 1969 the program of research of algorithmic logic was formulated in the Ph.D.  thesis of A. Salwicki.
-== Floyd-Hoare logic ==
+== Other logics of programs ==
-Paper of R.W. Floyd brought some light on proving programs correct.
+You may ask how calculus of programs is related to other calculi: e.g. Floyd, Hoare, Dijkstra, dynamic logic, etc.?
-Later C.A.R. Hoare proposed another formalization based on the ideas of Floyd.
+[[calculus of Floyd]]<br />
-S. Cook addressed the problem of completeness of Floyd-Hoare calculus and formulated the so called relative completeness theorem.
+[[logic of Hoare]]<br />
+[[calculus of weakest precondition of Dijkstra]]<br />
-In the light of the paper [{{Odn|ref=nie|Goraj, Mirkowska, Paluszkiewicz}}]   this theorem is unnecessary. Theorem 5 of this paper states that notions of feasible and of acceptable description 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. For the details see [{{Odn |ref=nie |AL4software }}] sections on Floyd's descriptions of programs and  Hoare's logic of partial correctness.
+[[dynamic logic]]<br />
 == Bibliography ==

@@ Linia 63: / Linia 63: @@
 [[Algorithmic theory of priority queues]]<br />
 <br />
 == History ==

@@ Linia 47: / Linia 47: @@
 [[Algorithmic theory of natural numbers]]<br />
 [[Algorithmic theory of integers]]<br />
- === Algorithmic theory of integers ===
+[[Algorithmic theory of FIFO queues]]<br />
 === Algorithmic theory of rational numbers ===
 == History ==