La lógica algorítmica es un cálculo de programas que permite la expresión de propiedades semánticas de los programas mediante fórmulas lógicas apropiadas . Proporciona un marco que permite probar las fórmulas a partir de los axiomas de las construcciones del programa, como las instrucciones de asignación, iteración y composición, y de los axiomas de las estructuras de datos en cuestión (véase Mirkowska y Salwicki (1987), Banachowski et al. (1977).
El siguiente diagrama ayuda a ubicar la lógica algorítmica entre otras lógicas .
El lenguaje formalizado de la lógica algorítmica (y de las teorías algorítmicas de varias estructuras de datos) contiene tres tipos de expresiones bien formadas: Términos - es decir, expresiones que denotan operaciones sobre elementos de estructuras de datos, fórmulas - es decir, expresiones que denotan las relaciones entre elementos de estructuras de datos, programas - es decir, algoritmos - estas expresiones describen los cálculos. Para la semántica de términos y fórmulas consulte las páginas sobre lógica de primer orden y semántica de Tarski. El significado de un programa es el conjunto de cálculos posibles del programa.
La lógica algorítmica es una de las muchas lógicas de los programas. Otra lógica de los programas es la lógica dinámica, véase lógica dinámica , Harel, Kozen y Tiuryn (2000).
![{\displaystyle \qquad \left[{\begin{array}{l}\mathrm {Lógica\ proposicional} \\o\\\mathrm {Cálculo\ oracional} \end{array}}\right]\subset \left[{\begin{array}{l}\mathrm {Cálculo\ de predicados} \\o\\\mathrm {Lógica\ de\ primer\ orden} \end{array}}\right]\subset \left[{\begin{array}{l}\mathrm {Cálculo\ de\ programas} \\o\\{\mbox{Lógica algorítmica}}\end{array}}\right]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b9a0144121e0bc509203574f211e1675d9ca1127)
