El cálculo proposicional clásico está caracterizado por una herramienta de inferencia visual llamada árboles de forzamiento semántico. Con esta herramienta se marcan los nodos del árbol asociado a una fórmula dada, con base en estas marcas se determina si la formula es valida o no. En caso de invalidez, la valuación que refuta la validez de la fórmula está determinada por las marcas de las hojas en su árbol de forzamiento. En caso de validez, se puede construir una deducción formal de la fórmula asociada a la raíz del árbol; esto se logra debido a que cada regla utilizada para marcar los nodos en el árbol está asociada a una regla de inferencia en el sistema deductivo.
Introducción
El método de los tableros semánticos, presentado por E. Beth en [1] y popularizado como árboles de opciones semánticas por R. Smullyan en [2], consiste básicamente en examinar, de manera sistemática, todas las posibilidades que podrían hacer falsa una proposición dada y buscar si una de estas posibilidades es lógicamente viable, es decir, que no genera contradicciones; en éste caso se tiene un contraejemplo que refuta la validez de la proposición dada; si no es posible generar un contraejemplo, esto es, ninguna posibilidad resulta lógicamente viable, entonces la proposición analizada es válida. Este método ha encontrado gran aceptación y se ha extendido a muchos sistemas de lógicas no clásicas, además, es fácil de implementar con un programa de computador.
Los árboles de forzamiento semántico, a diferencia de los árboles de opciones semánticas, no exploran todas las opciones posibles cuando se busca el contraejemplo, se limitan a las opciones que son deductivamente forzadas por las reglas del sistema. Por esta razón, el análisis de validez con árboles de forzamiento es en principio más sencillo y natural que con los árboles de opciones.
En este trabajo se presentan los árboles de forzamiento semántico a nivel proposicional para la lógica clásica (CL). Se prueba detalladamente la equivalencia entre la presentación semántica con valuaciones y la presentación con árboles de forzamiento. Esta caracterización permite, por un lado, si una fórmula es inválida, lo cual se concluye si el árbol de la fórmula está bien marcado, entonces la lectura de las marcas de los nodos asociados a las fórmulas atómicas proporciona una valuación que refuta la validez de la fórmula, y, por otro lado, si una fórmula es válida, lo cual se concluye si el árbol está mal marcado o si la raíz forzosamente está marcada con 1, entonces es posible construir una deducción formal con la cual se prueba que la fórmula asociada a la raíz del árbol es un teorema; para lograr esto se cambia cada regla para el forzamiento de marcas por la regla deductiva a la que está asociada.
2 Lenguaje de CL
El lenguaje de la Lógica Clásica (CL) consta de los operadores binarios →, ∧, ∨ y ↔, y del operador monádico ∼, además del paréntesis izquierdo y el paréntesis derecho. El conjunto de fórmulas de CL es generado por las siguientes reglas y sólo por ellas:
R1. Se tiene un conjunto enumerable de fórmulas atómicas.
Esta es una versión de prueba de citación de documentos de la Biblioteca Virtual Pro. Puede contener errores. Lo invitamos a consultar los manuales de citación de las respectivas fuentes.
Artículo:
Mejora del bloqueo en función de la dependencia para los sistemas de bases de datos de memoria principal
Artículo:
Coordinación de referencia en modo deslizante de sistemas de realimentación limitados
Artículo:
Un problema de gestión de inventarios multiproducto de un solo período bajo distribuciones de posibilidad variables
Artículo:
Utilización del modelo matemático sobre marketing de precisión con la informática de datos de transacciones en línea
Artículo:
Árboles de regresión granular difusa potenciada
Folleto:
Análisis de rentabilidad económica y financiera
Artículo:
¿Por qué debemos conservar la fauna silvestre?
Artículo:
Control y vigilancia de la calidad del agua de consumo humano
Manual:
Deshidratación y desecado de frutas, hortalizas y hongos. Procedimientos hogareños y comerciales de pequeña escala