Algorithmic logic (original) (raw)
Algorithmic logic is a calculus of programs that allows the expression of semantic properties of programs by appropriate logical formulas. It provides a framework that enables proving the formulas from the axioms of program constructs such as assignment, iteration and composition instructions and from the axioms of the data structures in question see , . Algorithmic logic is one of many logics of programs.Another logic of programs is dynamic logic, see dynamic logic, .
| Property | Value |
|---|---|
| dbo:abstract | Algorithmic logic is a calculus of programs that allows the expression of semantic properties of programs by appropriate logical formulas. It provides a framework that enables proving the formulas from the axioms of program constructs such as assignment, iteration and composition instructions and from the axioms of the data structures in question see , . The following diagram helps to locate algorithmic logic among other logics.The formalized language of algorithmic logic (and of algorithmic theories of various data structures) contains three types of well formed expressions: Terms - i.e. expressions denoting operations on elements of data structures, formulas - i.e. expressions denoting the relations among elements of data structures, programs - i.e. algorithms - these expressions describe the computations.For semantics of terms and formulas consult pages on first-order logic and Tarski's semantics. The meaning of a program is the set of possible computations of the program. Algorithmic logic is one of many logics of programs.Another logic of programs is dynamic logic, see dynamic logic, . (en) Logika algorytmiczna – rachunek logiczny, ale także rachunek programów. Każdy program możemy rozpatrywać jako modalność. Jeśli jest programem, a jest formułą, to wyrażenie postaci jest formułą algorytmiczną. W ten sposób mamy do czynienia ze splotem dwu algebr: algebry Boole’a i algebry programów. Znaczenie formuły jest wyznaczone gdy znamy znaczenie (tj. semantykę) programu i znaczenie formuły Przypomnijmy, że znaczeniem formuły (pierwszego rzędu) jest funkcja ze zbioru wartościowań zmiennych w zbiór {true, false} wartości logicznych. Znaczeniem programu jest funkcja (częściowa) ze zbioru wartościowań w ten sam zbiór. Teraz znaczenie formuły możemy opisać w następujący sposób: dla danego wartościowania zmiennych należy najpierw wyznaczyć wynik obliczenia programu i z kolei obliczyć wartość formuły dla wartościowania W przypadku gdy obliczenie programu dla wartościowania nie daje wyniku, przyjmujemy, że wartością formuły jest false. W języku logiki algorytmicznej można wyrażać semantyczne własności programów. Aksjomaty i reguły wnioskowania AL pozwalają na dowodzenie prawdziwych (semantycznie) formuł algorytmicznych. Oznacza to, że uzyskujemy możliwość dowodzenia faktów postaci: ten program jest poprawny względem warunku początkowego i warunku końcowego Formuła taka ma postać implikacji (pl) |
| dbo:wikiPageExternalLink | http://lem12.uksw.edu.pl/images/3/35/Algorithmic_Logic.pdf%7Cyear=1987%7Cpublisher=PWN https://archive.org/details/dynamiclogicfoun00davi_0%7Curl-access=registration%7C https://archive.org/details/dynamiclogicfoun00davi_0/page/459 http://lem12.uksw.edu.pl/images/4/42/Bcp211.pdf |
| dbo:wikiPageID | 42360188 (xsd:integer) |
| dbo:wikiPageLength | 3058 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1100555745 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Algorithm dbr:Dynamic_logic_(modal_logic) dbr:Mathematical_logic dbr:Data_structure dbr:First-order_logic dbr:Formula dbr:Semantic_property dbr:Term_(logic) dbc:Algorithms dbc:Theoretical_computer_science dbr:Axiom dbr:Software_framework |
| dbp:wikiPageUsesTemplate | dbt:Cite_book dbt:Harvtxt dbt:Original_research dbt:Mathlogic-stub |
| dct:subject | dbc:Algorithms dbc:Theoretical_computer_science |
| rdf:type | yago:Abstraction100002137 yago:Act100030358 yago:Activity100407535 yago:Algorithm105847438 yago:Event100029378 yago:Procedure101023820 yago:PsychologicalFeature100023100 yago:YagoPermanentlyLocatedEntity yago:Rule105846932 yago:WikicatAlgorithms |
| rdfs:comment | Algorithmic logic is a calculus of programs that allows the expression of semantic properties of programs by appropriate logical formulas. It provides a framework that enables proving the formulas from the axioms of program constructs such as assignment, iteration and composition instructions and from the axioms of the data structures in question see , . Algorithmic logic is one of many logics of programs.Another logic of programs is dynamic logic, see dynamic logic, . (en) Logika algorytmiczna – rachunek logiczny, ale także rachunek programów. Każdy program możemy rozpatrywać jako modalność. Jeśli jest programem, a jest formułą, to wyrażenie postaci jest formułą algorytmiczną. W ten sposób mamy do czynienia ze splotem dwu algebr: algebry Boole’a i algebry programów. Znaczenie formuły jest wyznaczone gdy znamy znaczenie (tj. semantykę) programu i znaczenie formuły Przypomnijmy, że znaczeniem formuły (pierwszego rzędu) jest funkcja ze zbioru wartościowań zmiennych w zbiór {true, false} wartości logicznych. Znaczeniem programu jest funkcja (częściowa) ze zbioru wartościowań w ten sam zbiór. Teraz znaczenie formuły możemy opisać w następujący sposób: dla danego wartościowania zmiennych należy najpierw wyznaczyć wynik obliczenia programu i z kolei oblic (pl) |
| rdfs:label | Algorithmic logic (en) Logika algorytmiczna (pl) |
| owl:sameAs | freebase:Algorithmic logic yago-res:Algorithmic logic wikidata:Algorithmic logic dbpedia-pl:Algorithmic logic https://global.dbpedia.org/id/Diwp |
| prov:wasDerivedFrom | wikipedia-en:Algorithmic_logic?oldid=1100555745&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Algorithmic_logic |
| is dbo:wikiPageWikiLink of | dbr:Dynamic_logic_(modal_logic) dbr:Laurie_Spiegel |
| is foaf:primaryTopic of | wikipedia-en:Algorithmic_logic |