algorithmic logic

{{Short description|Logic for mathematics}}

{{Original research|date=February 2016}}

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 {{harvtxt|Mirkowska|Salwicki|1987}}, {{harvtxt|Banachowski|Kreczmar|Mirkowska|Rasiowa|1977}}.

The following diagram helps to locate algorithmic logic among other logics.

$\backslash qquad\; \backslash left\; [\backslash begin\{array\}\{l\}\; \backslash mathrm\{Propositional\backslash \; logic\}\backslash \backslash or\; \backslash \backslash \; \backslash mathrm\{Sentential\backslash \; calculus\}\; \backslash end\{array\}\backslash right\; ]\backslash subset\; \backslash left\; [\backslash begin\{array\}\{l\}\; \backslash mathrm\{Predicate\backslash \; calculus\}\; \backslash \backslash or\; \backslash \backslash \; \backslash mathrm\{First\backslash \; order\backslash \; logic\}\backslash end\{array\}\backslash right\; ]\; \backslash subset\; \backslash left\; [\backslash begin\{array\}\{l\}\backslash mathrm\{Calculus\backslash \; of\backslash \; programs\}\backslash \backslash or\; \backslash \backslash \; \backslash mbox\{Algorithmic\; logic\}\; \backslash end\{array\}\backslash right\; ]$

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 $K$ 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, {{harvtxt|Harel|Kozen|Tiuryn|2000}}.