La lógica de ecuaciones de primer orden consiste en términos libres de cuantificadores de la lógica de primer orden ordinaria , con la igualdad como único símbolo de predicado . La teoría del modelo de esta lógica fue desarrollada en álgebra universal por Birkhoff , Grätzer y Cohn . Más tarde se hizo en una rama de la teoría de la categoría por Lawvere ( "teorías algebraicas"). [1]
Los términos de la lógica de las ecuaciones se construyen a partir de variables y constantes que utilizan símbolos de función (u operaciones).
Silogismo
Aquí están las cuatro reglas de inferencia de la lógica. denota sustitución textual de expresión para variable en expresión . Próximo, denota igualdad, por y del mismo tipo, mientras , o equivalencia, se define solo para y de tipo booleano . Para y de tipo booleano, y tienen el mismo significado.
Sustitución | Si es un teorema, entonces también lo es . | |
---|---|---|
Leibniz | Si es un teorema, entonces también lo es . | |
Transitividad | Si y son teoremas, entonces también lo es . | |
Ecuanimidad | Si y son teoremas, entonces también lo es . |
Historia
La lógica ecuacional fue desarrollada a lo largo de los años (a principios de la década de 1980) por investigadores en el desarrollo formal de programas, que sintieron la necesidad de un estilo efectivo de manipulación, de cálculo. Participaron personas como Roland Carl Backhouse , Edsger W. Dijkstra , Wim HJ Feijen, David Gries , Carel S. Scholten y Netty van Gasteren. Wim Feijen es responsable de los detalles importantes del formato de prueba.
Los axiomas son similares a los utilizados por Dijkstra y Scholten en su monografía Cálculo de predicados y semántica de programas (Springer Verlag, 1990), pero nuestro orden de presentación es ligeramente diferente.
En su monografía, Dijkstra y Scholten utilizan las tres reglas de inferencia Leibniz, sustitución y transitividad. Sin embargo, el sistema Dijkstra / Scholten no es una lógica, como los lógicos usan la palabra. Algunas de sus manipulaciones se basan en los significados de los términos involucrados y no en reglas sintácticas de manipulación claramente presentadas. El primer intento de convertirlo en una lógica real apareció en A Logical Approach to Discrete Math . Sin embargo, falta la regla de inferencia Ecuanimidad, y la definición de teorema está distorsionada para explicarla. La introducción de Equanimity y su uso en el formato de prueba se debe a Gries y Schneider. Se utiliza, por ejemplo, en las pruebas de solidez e integridad, y aparecerá en la segunda edición de A Logical Approach to Discrete Math . [2]
Prueba
Explicamos cómo se usan las cuatro reglas de inferencia en las demostraciones, usando la prueba de . Los símbolos lógicos y indican "verdadero" y "falso", respectivamente, y indica "no". Los números del teorema se refieren a los teoremas de A Logical Approach to Discrete Math . [2]
Primero, líneas - mostrar un uso de la regla de inferencia de Leibniz:
es la conclusión de Leibniz, y su premisa se da en línea . Del mismo modo, la igualdad en líneas- se fundamentan utilizando Leibniz.
La "pista" en línea se supone que da una premisa de Leibniz, mostrando qué sustitución de iguales por iguales se está utilizando. Esta premisa es el teorema con la sustitución , es decir
Esto muestra cómo se usa la sustitución de la regla de inferencia dentro de las sugerencias.
De y , concluimos por la regla de inferencia de la Transitividad que . Esto muestra cómo se usa la Transitividad.
Finalmente, tenga en cuenta esa línea , , es un teorema, como lo indica la sugerencia a su derecha. Por lo tanto, por regla de inferencia Ecuanimidad, concluimos que la líneatambién es un teorema. Yes lo que queríamos demostrar. [2]
Referencias
- ^ lógica ecuacional. (Dakota del Norte). Diccionario gratuito de informática en línea. Obtenido el 24 de octubre de 2011 del sitio web Dictionary.com: http://dictionary.reference.com/browse/equational+logic
- ↑ a b c d Gries, D. (2010). Introducción a la lógica ecuacional. Obtenido de http://www.cs.cornell.edu/home/gries/Logic/Equational.html