Método de cuadros analíticos
En teoría de la prueba , el cuadro semántico ( / t æ b l oʊ , t æ b l oʊ / ; plural: cuadros , también llamado árbol de verdad ) es un procedimiento de decisión para oracionales lógicas y relacionados, y un procedimiento de prueba para las fórmulas de lógica de primer orden. Un cuadro analítico es una estructura de árbol calculada para una fórmula lógica, que tiene en cada nodo una subfórmula de la fórmula original para ser probada o refutada. La computación construye este árbol y lo usa para probar o refutar toda la fórmula. El método del cuadro también puede determinar la satisfacibilidad de conjuntos finitos de fórmulas de varias lógicas. Es el procedimiento de prueba más popular para lógicas modales (Girle 2000).
Para los cuadros de refutación, el objetivo es mostrar que la negación de una fórmula no se puede satisfacer. Hay reglas para manejar cada uno de los conectivos habituales , comenzando por el conectivo principal. En muchos casos, la aplicación de estas reglas hace que el subtableau se divida en dos. Se instancian los cuantificadores . Si alguna rama de un cuadro lleva a una contradicción evidente , la rama se cierra . Si todas las ramas se cierran, la prueba está completa y la fórmula original es una verdad lógica .
Aunque la idea fundamental detrás del método del cuadro analítico se deriva del teorema de eliminación de cortes de la teoría de la prueba estructural , los orígenes de los cálculos del cuadro se encuentran en el significado (o semántica ) de los conectivos lógicos, ya que la conexión con la teoría de la prueba se hizo solo en décadas recientes.
Más específicamente, un cálculo de cuadro consiste en una colección finita de reglas y cada regla especifica cómo dividir una conectiva lógica en sus partes constituyentes. Las reglas normalmente se expresan en términos de conjuntos finitos de fórmulas, aunque existen lógicas para las que debemos utilizar estructuras de datos más complicadas, como multijuegos , listas o incluso árboles de fórmulas. De ahora en adelante, "set" denota cualquiera de {set, multiset, list, tree}.
Si existe tal regla para cada conectivo lógico, entonces el procedimiento eventualmente producirá un conjunto que consiste solo en fórmulas atómicas y sus negaciones, que no se pueden descomponer más. Tal conjunto es fácilmente reconocible como satisfactorio o insatisfactorio con respecto a la semántica de la lógica en cuestión. Para realizar un seguimiento de este proceso, los nodos de un cuadro en sí se establecen en forma de árbol y las ramas de este árbol se crean y evalúan de manera sistemática. Un método tan sistemático para buscar en este árbol da lugar a un algoritmo para realizar deducción y razonamiento automatizado. Tenga en cuenta que este árbol más grande está presente independientemente de si los nodos contienen conjuntos, conjuntos múltiples, listas o árboles.
Esta sección presenta el cálculo del cuadro para la lógica proposicional clásica. Un cuadro comprueba si un determinado conjunto de fórmulas es satisfactorio o no. Se puede utilizar para comprobar la validez o la vinculación: una fórmula es válida si su negación es insatisfactorio y las fórmulas implican si es insatisfactorio.
