En teoría de la prueba , el cuadro semántico ( / t æ ˈ b l oʊ , ˈ t æ b l oʊ / ; plural: tableaux , también llamado árbol de verdad ) es un procedimiento de decisión para lógicas oracionales y relacionadas, y un procedimiento de prueba para 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 que se debe probar o refutar. La computación construye este árbol y lo utiliza para probar o refutar toda la fórmula. [1] El método del cuadro también puede determinar la satisfacibilidad de conjuntos finitos de fórmulas de diversas lógicas. Es el procedimiento de prueba más popular para lógicas modales . [2]
En su Lógica simbólica Parte II , Charles Lutwidge Dodgson (también conocido por su seudónimo literario, Lewis Carroll) introdujo el Método de los árboles, el primer uso moderno de un árbol de verdad. [3]
El método de los cuadros semánticos fue inventado por el lógico holandés Evert Willem Beth (Beth 1955) [4] y simplificado, para la lógica clásica, por Raymond Smullyan (Smullyan 1968, 1995). [5] Es la simplificación de Smullyan, los "cuadros unilaterales", lo que se describe aquí. El método de Smullyan ha sido generalizado a lógicas arbitrarias proposicionales y de primer orden de muchos valores por Walter Carnielli (Carnielli 1987). [6] Tableaux puede verse intuitivamente como sistemas sucesivos al revés. Esta relación simétrica entre cuadros y sistemas sucesivos se estableció formalmente en (Carnielli 1991). [7]
En el caso de los cuadros de refutación, el objetivo es mostrar que la negación de una fórmula no puede satisfacerse. Existen reglas para el manejo de cada uno de los conectivos habituales , comenzando por el conectivo principal. En muchos casos, la aplicación de estas reglas hace que el subcuadro se divida en dos. Se crean instancias de los cuantificadores . Si alguna rama de un cuadro conduce 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 sólo en décadas recientes. [ se necesita aclaración ]
Más específicamente, un cálculo de cuadro consta de una colección finita de reglas y cada regla especifica cómo descomponer un conectivo lógico en sus partes constituyentes. Las reglas normalmente se expresan en términos de conjuntos finitos de fórmulas, aunque hay lógicas para las que debemos utilizar estructuras de datos más complicadas, como conjuntos múltiples , listas o incluso árboles de fórmulas. De ahora en adelante, "conjunto" denota cualquiera de {conjunto, multiconjunto, lista, árbol}.
Si existe tal regla para cada conectivo lógico, entonces el procedimiento producirá eventualmente un conjunto que consta sólo de fórmulas atómicas y sus negaciones, que no pueden descomponerse más. Un conjunto así es fácilmente reconocible como satisfactible 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 disponen en forma de árbol y las ramas de este árbol se crean y evalúan de forma sistemática. Un método tan sistemático para buscar en este árbol da lugar a un algoritmo para realizar deducciones y razonamientos automatizados. 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 de cuadro para la lógica proposicional clásica. Un cuadro comprueba si un conjunto determinado 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 insatisfactoria y las fórmulas implican si es insatisfactoria.
El principio fundamental de los cuadros proposicionales es intentar "dividir" fórmulas complejas en otras más pequeñas hasta que se produzcan pares complementarios de literales o no sea posible una mayor expansión.
El método funciona en un árbol cuyos nodos están etiquetados con fórmulas. En cada paso, este árbol se modifica; en el caso proposicional, los únicos cambios permitidos son las adiciones de un nodo como descendiente de una hoja. El procedimiento comienza generando el árbol formado por una cadena de todas las fórmulas del conjunto para demostrar la insatisfacción. [8] Entonces, el siguiente procedimiento puede aplicarse repetidamente de forma no determinista:
Con el tiempo, este procedimiento terminará, porque en algún momento se aplican todos los nodos aplicables y las reglas de expansión garantizan que cada nodo del árbol sea más simple que el nodo aplicable utilizado para crearlo.
El principio del cuadro es que las fórmulas en nodos de la misma rama se consideran en conjunto, mientras que las diferentes ramas se consideran disyuntas. Como resultado, un cuadro es una representación en forma de árbol de una fórmula que es una disyunción de conjunciones. Esta fórmula es equivalente al conjunto para demostrar la insatisfacibilidad. El procedimiento modifica el cuadro de tal manera que la fórmula representada por el cuadro resultante sea equivalente a la original. Una de estas conjunciones puede contener un par de literales complementarios, en cuyo caso se demuestra que esa conjunción es insatisfactoria. Si se demuestra que todas las conjunciones son insatisfactorias, el conjunto original de fórmulas es insatisfactorio.
Siempre que una rama de un cuadro contiene una fórmula que es la conjunción de dos fórmulas, ambas fórmulas son consecuencias de esa fórmula. Este hecho puede formalizarse mediante la siguiente regla para la expansión de un cuadro:
( ) Si una rama del cuadro contiene una fórmula conjuntiva , agregue a su hoja la cadena de dos nodos que contienen las fórmulas y
Esta regla generalmente se escribe de la siguiente manera:
Una variante de esta regla permite que un nodo contenga un conjunto de fórmulas en lugar de una sola. En este caso, las fórmulas de este conjunto se consideran en conjunto, por lo que se pueden agregar al final de una rama que contenga . Más precisamente, si un nodo en una rama está etiquetado , se puede agregar a la rama la nueva hoja .
Si una rama de un cuadro contiene una fórmula que es una disyunción de dos fórmulas, como , se puede aplicar la siguiente regla:
( ) Si un nodo en una rama contiene una fórmula disyuntiva , entonces cree dos hijos hermanos en la hoja de la rama, que contengan las fórmulas y , respectivamente.
Esta regla divide una rama en dos, diferenciándose sólo en el nodo final. Dado que las ramas se consideran en disyunción entre sí, las dos ramas resultantes son equivalentes a la original, ya que la disyunción de sus nodos no comunes es precisamente . La regla de disyunción generalmente se escribe formalmente utilizando el símbolo para separar las fórmulas de los dos nodos distintos que se crearán:
Si se supone que los nodos contienen conjuntos de fórmulas, esta regla se reemplaza por: si un nodo está etiquetado como , a una hoja de la rama en la que se encuentra este nodo se le pueden agregar dos nodos secundarios hermanos etiquetados y , respectivamente.
El objetivo de los cuadros es generar fórmulas progresivamente más simples hasta que se produzcan pares de literales opuestos o no se pueda aplicar ninguna otra regla. La negación se puede tratar haciendo inicialmente fórmulas en forma normal de negación , de modo que la negación solo ocurra delante de los literales. Alternativamente, se pueden utilizar las leyes de De Morgan durante la expansión del cuadro, de modo que, por ejemplo, se trate como . En este caso también se utilizan reglas que introducen o eliminan un par de negaciones (como en ) (de lo contrario, no habría forma de expandir una fórmula como :
Cada cuadro puede considerarse como una representación gráfica de una fórmula, que equivale al conjunto a partir del cual se construye el cuadro. Esta fórmula es la siguiente: cada rama del cuadro representa la conjunción de sus fórmulas; el cuadro representa la disyunción de sus ramas. Las reglas de expansión transforman un cuadro en uno que tiene una fórmula representada equivalente. Dado que el cuadro se inicializa como una única rama que contiene las fórmulas del conjunto de entrada, todos los cuadros posteriores obtenidos de él representan fórmulas que son equivalentes a ese conjunto (en la variante donde el cuadro inicial es el nodo único etiquetado como verdadero, las fórmulas representadas por Los cuadros son consecuencias del conjunto original.)
El método de cuadros funciona comenzando con el conjunto inicial de fórmulas y luego agregando al cuadro fórmulas cada vez más simples hasta que la contradicción se muestra en la forma simple de literales opuestos. Dado que la fórmula representada por un cuadro es la disyunción de las fórmulas representadas por sus ramas, la contradicción se obtiene cuando cada rama contiene un par de literales opuestos.
Una vez que una rama contiene un literal y su negación, su fórmula correspondiente es insatisfactoria. Como resultado, esta sucursal ahora puede "cerrarse", ya que no es necesario ampliarla más. Si todas las ramas de un cuadro están cerradas, la fórmula representada por el cuadro es insatisfactoria; por lo tanto, el conjunto original también es insatisfactorio. Obtener un cuadro donde todas las ramas estén cerradas es una forma de demostrar la insatisfacción del conjunto original. En el caso proposicional, también se puede demostrar que la satisfacibilidad se demuestra por la imposibilidad de encontrar un cuadro cerrado, siempre que cada regla de expansión se haya aplicado en todos los lugares en los que podría aplicarse. En particular, si un cuadro contiene algunas ramas abiertas (no cerradas) y cada fórmula que no es literal ha sido utilizada por una regla para generar un nuevo nodo en cada rama en la que se encuentra la fórmula, el conjunto es satisfactorio.
Esta regla tiene en cuenta que una fórmula puede aparecer en más de una rama (este es el caso si hay al menos un punto de bifurcación "debajo" del nodo). En este caso, se debe aplicar la regla para expandir la fórmula de modo que sus conclusiones se agreguen a todas estas ramas que aún están abiertas, antes de que uno pueda concluir que el cuadro no se puede expandir más y que, por lo tanto, la fórmula es satisfactoria.
Una variante del cuadro es etiquetar los nodos con conjuntos de fórmulas en lugar de fórmulas únicas. En este caso, el cuadro inicial es un nodo único etiquetado con el conjunto que se ha de demostrar que es satisfactorio. Por lo tanto, se considera que las fórmulas de un conjunto están en conjunción.
Las reglas de expansión del cuadro ahora pueden funcionar en las hojas del cuadro, ignorando todos los nodos internos. Para la conjunción, la regla se basa en la equivalencia de un conjunto que contiene una conjunción con el conjunto que contiene ambas y en lugar de ella. En particular, si una hoja está etiquetada con , se le puede agregar un nodo con la etiqueta :
Para la disyunción, un conjunto es equivalente a la disyunción de los dos conjuntos y . Como resultado, si el primer conjunto etiqueta una hoja, se le pueden agregar dos hijos, etiquetados con las dos últimas fórmulas.
Finalmente, si un conjunto contiene tanto un literal como su negación, esta rama se puede cerrar:
Un cuadro para un conjunto finito dado X es un árbol finito (al revés) con raíz X en el que todos los nodos secundarios se obtienen aplicando las reglas del cuadro a sus padres. Una rama en dicho cuadro está cerrada si su nodo hoja contiene "cerrado". Un cuadro está cerrado si todas sus ramas están cerradas. Un cuadro está abierto si al menos una rama no está cerrada.
A continuación se muestran dos cuadros cerrados para el conjunto.
Cada aplicación de regla está marcada en el lado derecho. Ambos consiguen el mismo efecto, el primero cierra más rápido. La única diferencia es el orden en que se realiza la reducción.
y el segundo, más largo, con las reglas aplicadas en diferente orden:
El primer cuadro se cierra después de una sola aplicación de la regla, mientras que el segundo no da en el blanco y tarda mucho más en cerrarse. Claramente, preferiríamos encontrar siempre los cuadros cerrados más cortos, pero se puede demostrar que no puede existir un único algoritmo que encuentre los cuadros cerrados más cortos para todos los conjuntos de fórmulas de entrada.
Las tres reglas dadas anteriormente son suficientes para decidir si un conjunto dado de fórmulas en forma normal negada son conjuntamente satisfactorias:
Simplemente aplique todas las reglas posibles en todos los órdenes posibles hasta que encontremos un cuadro cerrado para o hasta que agotemos todas las posibilidades y concluyamos que cada cuadro para está abierto.
En el primer caso, es conjuntamente insatisfactorio y en el segundo, el nodo hoja de la rama abierta asigna una asignación a las fórmulas atómicas y a las fórmulas atómicas negadas que lo hace conjuntamente satisfactorio. La lógica clásica en realidad tiene la propiedad bastante interesante de que necesitamos investigar solo (cualquier) cuadro por completo: si se cierra, entonces es insatisfactorio y si está abierto, entonces es satisfacible. Pero otras lógicas generalmente no disfrutan de esta propiedad.
Estas reglas son suficientes para toda la lógica clásica al tomar un conjunto inicial de fórmulas X y reemplazar cada miembro C por su forma normal negada lógicamente equivalente C', dando un conjunto de fórmulas X' . Sabemos que X es satisfactible si y sólo si X' es satisfacible, por lo que basta buscar un cuadro cerrado para X' utilizando el procedimiento descrito anteriormente.
Al establecer podemos probar si la fórmula A es una tautología de la lógica clásica:
Si el cuadro para cierres entonces es insatisfactorio y entonces A es una tautología ya que ninguna asignación de valores de verdad hará que A sea falso. De lo contrario, cualquier hoja abierta de cualquier rama abierta de cualquier cuadro abierto da una asignación que falsifica A .
La lógica proposicional clásica suele tener un conectivo para denotar implicación material . Si escribimos este conectivo como ⇒, entonces la fórmula A ⇒ B significa "si A entonces B ". Es posible dar una regla para descomponer A ⇒ B en sus fórmulas constituyentes. De manera similar, podemos dar una regla para descomponer cada uno de ¬( A ∧ B ), ¬( A ∨ B ), ¬(¬ A ) y ¬( A ⇒ B ). Juntas, estas reglas proporcionarían un procedimiento final para decidir si un conjunto dado de fórmulas es simultáneamente satisfactorio en la lógica clásica, ya que cada regla descompone una fórmula en sus constituyentes, pero ninguna regla construye fórmulas más grandes a partir de constituyentes más pequeños. Por lo tanto, eventualmente debemos llegar a un nodo que contenga sólo átomos y negaciones de átomos. Si este último nodo coincide con (id) entonces podemos cerrar la rama, de lo contrario permanece abierta.
Pero tenga en cuenta que las siguientes equivalencias se mantienen en la lógica clásica donde (...) = (...) significa que la fórmula del lado izquierdo es lógicamente equivalente a la fórmula del lado derecho:
Si comenzamos con una fórmula arbitraria C de lógica clásica y aplicamos estas equivalencias repetidamente para reemplazar los lados izquierdos con los lados derechos en C , entonces obtendremos una fórmula C' que es lógicamente equivalente a C pero que tiene la propiedad que C' no contiene implicaciones y que ¬ aparece sólo delante de fórmulas atómicas. Se dice que tal fórmula está en forma normal de negación y es posible demostrar formalmente que cada fórmula C de la lógica clásica tiene una fórmula lógicamente equivalente C' en forma normal de negación. Es decir, C es satisfactible si y sólo si C' es satisfacible.
Las reglas anteriores para el cuadro proposicional se pueden simplificar utilizando notación uniforme. En notación uniforme, cada fórmula es de tipo (alfa) o de tipo (beta). A cada fórmula de tipo alfa se le asignan los dos componentes , y a cada fórmula de tipo beta se le asignan los dos componentes . Se puede considerar que las fórmulas de tipo alfa son conjuntivas, ya que ambas y están implícitas en ser verdaderas. Se puede considerar que las fórmulas de tipo beta son disyuntivas, ya que o está implícito en ser verdadera. Las siguientes tablas muestran cómo determinar el tipo y los componentes de cualquier fórmula proposicional dada:
En cada tabla, la columna de la izquierda muestra todas las estructuras posibles para las fórmulas de tipo alfa o beta, y las columnas de la derecha muestran sus respectivos componentes. Alternativamente, las reglas para la notación uniforme se pueden expresar utilizando fórmulas con signo:
Al construir un cuadro proposicional usando la notación anterior, cada vez que uno encuentra una fórmula de tipo alfa, sus dos componentes se agregan a la rama actual que se está expandiendo. Siempre que uno encuentre una fórmula de tipo beta en alguna rama , puede dividirla en dos ramas, una con el conjunto { , } de fórmulas y la otra con el conjunto { , } de fórmulas. [10]
Los cuadros se extienden a la lógica de predicados de primer orden mediante dos reglas para tratar con cuantificadores universales y existenciales, respectivamente. Se pueden utilizar dos conjuntos diferentes de reglas; Ambos emplean una forma de Skolemización para manejar cuantificadores existenciales, pero difieren en el manejo de cuantificadores universales.
Aquí se supone que el conjunto de fórmulas para comprobar la validez no contiene variables libres; Esto no es una limitación ya que las variables libres se cuantifican implícitamente universalmente, por lo que se pueden agregar cuantificadores universales sobre estas variables, lo que da como resultado una fórmula sin variables libres.
Una fórmula de primer orden implica todas las fórmulas donde hay un término fundamental . Por tanto, la siguiente regla de inferencia es correcta:
Al contrario de lo que ocurre con las reglas de las conectivas proposicionales, pueden ser necesarias múltiples aplicaciones de esta regla a la misma fórmula. Como ejemplo, solo se puede demostrar que el conjunto es insatisfactorio si ambos y se generan a partir de .
Los cuantificadores existenciales se tratan mediante la Skolemización. En particular, una fórmula con un cuantificador existencial principal como genera su eskolemización , donde hay un nuevo símbolo constante.
El término de Skolem es una constante (una función de aridad 0) porque la cuantificación excesiva no ocurre dentro del alcance de ningún cuantificador universal. Si la fórmula original contenía algunos cuantificadores universales de modo que la cuantificación final estaba dentro de su alcance, estos cuantificadores evidentemente han sido eliminados mediante la aplicación de la regla para los cuantificadores universales.
La regla de los cuantificadores existenciales introduce nuevos símbolos constantes. Estos símbolos pueden ser utilizados por la regla para cuantificadores universales, de modo que se pueden generar incluso si no estaban en la fórmula original sino que es una constante de Skolem creada por la regla para cuantificadores existenciales.
Las dos reglas anteriores para los cuantificadores universales y existenciales son correctas, al igual que las reglas proposicionales: si un conjunto de fórmulas genera un cuadro cerrado, este conjunto es insatisfactorio. También se puede demostrar la integridad: si un conjunto de fórmulas es insatisfactorio, existe un cuadro cerrado construido a partir de él mediante estas reglas. Sin embargo, encontrar un cuadro tan cerrado requiere una política adecuada de aplicación de reglas. De lo contrario, un conjunto insatisfactorio puede generar un cuadro de crecimiento infinito. Por ejemplo, el conjunto es insatisfactorio, pero nunca se obtiene un cuadro cerrado si uno sigue aplicando imprudentemente la regla de los cuantificadores universales a , generando, por ejemplo , . Siempre se puede encontrar un cuadro cerrado descartando ésta y otras políticas "injustas" similares de aplicación de las reglas del cuadro.
La regla para los cuantificadores universales es la única regla no determinista, ya que no especifica con qué término instanciar. Además, mientras que las otras reglas deben aplicarse solo una vez para cada fórmula y cada ruta en la que se encuentra la fórmula, esta puede requerir múltiples aplicaciones. Sin embargo, la aplicación de esta regla puede restringirse retrasando su aplicación hasta que no sea aplicable otra regla y restringiendo la aplicación de la regla a términos básicos que ya aparecen en el recorrido del cuadro. La variante de cuadros con unificación que se muestra a continuación tiene como objetivo resolver el problema del no determinismo.
El principal problema del cuadro sin unificación es cómo elegir un término fundamental para la regla del cuantificador universal. De hecho, se pueden utilizar todos los términos básicos posibles, pero claramente la mayoría de ellos podrían ser inútiles para cerrar el cuadro.
Una solución a este problema es "retrasar" la elección del término hasta el momento en que el consecuente de la regla permita cerrar al menos una rama del cuadro. Esto se puede hacer usando una variable en lugar de un término, de modo que genere y luego permitiendo sustituciones para luego reemplazarla con un término. La regla para los cuantificadores universales es:
Si bien se supone que el conjunto inicial de fórmulas no contiene variables libres, una fórmula del cuadro puede contener las variables libres generadas por esta regla. Estas variables libres se consideran implícitamente cuantificadas universalmente.
Esta regla emplea una variable en lugar de un término fundamental. Lo que se gana con este cambio es que a estas variables se les puede dar un valor cuando se puede cerrar una rama del cuadro, resolviendo el problema de generar términos que podrían ser inútiles.
Como ejemplo, se puede demostrar que es insatisfactorio generando primero ; la negación de este literal es unificable con , siendo el unificador más general la sustitución que reemplaza por ; La aplicación de esta sustitución da como resultado la sustitución por , lo que cierra el cuadro.
Esta regla cierra al menos una rama del cuadro: la que contiene el par de literales considerado. Sin embargo, la sustitución debe aplicarse a todo el cuadro, no sólo a estos dos literales. Esto se expresa diciendo que las variables libres del cuadro son rígidas : si una aparición de una variable se reemplaza por otra cosa, todas las demás apariciones de la misma variable deben reemplazarse de la misma manera. Formalmente, las variables libres se cuantifican (implícitamente) universalmente y todas las fórmulas del cuadro están dentro del alcance de estos cuantificadores.
La Skolemización se ocupa de los cuantificadores existenciales. Al contrario del cuadro sin unificación, los términos de Skolem pueden no ser constantes simples. De hecho, las fórmulas en un cuadro con unificación pueden contener variables libres, que implícitamente se consideran universalmente cuantificadas. Como resultado, una fórmula como ésta puede estar dentro del alcance de los cuantificadores universales; si este es el caso, el término de Skolem no es una simple constante sino un término formado por un nuevo símbolo de función y las variables libres de la fórmula.
Esta regla incorpora una simplificación respecto de una regla donde están las variables libres de la rama, no de solas. Esta regla se puede simplificar aún más reutilizando un símbolo de función si ya se ha utilizado en una fórmula que es idéntica hasta el cambio de nombre de variable.
La fórmula representada por un cuadro se obtiene de forma similar al caso proposicional, con el supuesto adicional de que las variables libres se consideran universalmente cuantificadas. En cuanto al caso proposicional, las fórmulas de cada rama están unidas y las fórmulas resultantes están separadas. Además, todas las variables libres de la fórmula resultante están cuantificadas universalmente. Todos estos cuantificadores tienen la fórmula completa en su alcance. En otras palabras, si la fórmula se obtiene al desunir la conjunción de las fórmulas en cada rama, y las variables libres en ella, entonces la fórmula está representada por el cuadro. Se aplican las siguientes consideraciones:
Las dos variantes siguientes también son correctas.
Los cuadros con unificación pueden demostrarse completos: si un conjunto de fórmulas es insatisfactorio, tiene una prueba de cuadro con unificación. Sin embargo, encontrar tal prueba puede ser un problema difícil. Al contrario del caso sin unificación, la aplicación de una sustitución puede modificar la parte existente de un cuadro; Si bien la aplicación de una sustitución cierra al menos una rama, puede hacer que sea imposible cerrar otras ramas (incluso si el conjunto es insatisfactorio).
Una solución a este problema es la creación de instancias retrasada : no se aplica ninguna sustitución hasta que se encuentre una que cierre todas las ramas al mismo tiempo. Con esta variante, siempre se puede encontrar una prueba para un conjunto insatisfactorio mediante una política adecuada de aplicación de las otras reglas. Sin embargo, este método requiere que todo el cuadro se mantenga en la memoria: el método general cierra ramas, que luego pueden descartarse, mientras que esta variante no cierra ninguna rama hasta el final.
El problema de que algunos cuadros que pueden generarse son imposibles de cerrar incluso si el conjunto es insatisfactorio es común a otros conjuntos de reglas de expansión del cuadro: incluso si algunas secuencias específicas de aplicación de estas reglas permiten construir un cuadro cerrado (si el conjunto es insatisfactorio ), algunas otras secuencias conducen a cuadros que no se pueden cerrar. Las soluciones generales para estos casos se describen en la sección "Búsqueda de un cuadro".
Un cálculo de cuadro es un conjunto de reglas que permiten construir y modificar un cuadro. Las reglas del cuadro proposicional, las reglas del cuadro sin unificación y las reglas del cuadro con unificación son todas cálculos del cuadro. Algunas propiedades importantes que un cálculo de cuadro puede poseer o no son la integridad, la destructividad y la confluencia de pruebas.
Un cálculo de cuadro se considera completo si permite construir una prueba de cuadro para cada conjunto de fórmulas insatisfactorio dado. Los cálculos del cuadro mencionados anteriormente pueden demostrarse completos.
Una diferencia notable entre el cuadro con unificación y los otros dos cálculos es que los dos últimos cálculos solo modifican un cuadro al agregarle nuevos nodos, mientras que el primero permite sustituciones para modificar la parte existente del cuadro. De manera más general, los cálculos de Tableau se clasifican como destructivos o no destructivos dependiendo de si solo agregan nuevos nodos al Tableau o no. Por lo tanto, el cuadro con unificación es destructivo, mientras que el cuadro proposicional y el cuadro sin unificación no son destructivos.
La confluencia de pruebas es la propiedad de un cálculo de cuadro que permite obtener una prueba para un conjunto arbitrario insatisfactorio a partir de un cuadro arbitrario, suponiendo que este cuadro se haya obtenido aplicando las reglas del cálculo. En otras palabras, en un cálculo de cuadro de prueba confluente, a partir de un conjunto insatisfactorio se puede aplicar cualquier conjunto de reglas y aun así obtener un cuadro del que se puede obtener uno cerrado aplicando algunas otras reglas.
Un cálculo de cuadro es simplemente un conjunto de reglas que prescriben cómo se puede modificar un cuadro. Un procedimiento de prueba es un método para encontrar una prueba (si existe). En otras palabras, un cálculo de cuadro es un conjunto de reglas, mientras que un procedimiento de prueba es una política de aplicación de estas reglas. Incluso si un cálculo es completo, no todas las posibles opciones de aplicación de reglas conducen a la prueba de un conjunto insatisfactorio. Por ejemplo, es insatisfactorio, pero tanto los cuadros con unificación como los cuadros sin unificación permiten que la regla de los cuantificadores universales se aplique repetidamente a la última fórmula, mientras que simplemente aplicar la regla de disyunción a la tercera conduciría directamente al cierre.
Para los procedimientos de prueba, se ha dado una definición de completitud: un procedimiento de prueba es fuertemente completo si permite encontrar un cuadro cerrado para cualquier conjunto de fórmulas insatisfactorio dado. La confluencia de la prueba del cálculo subyacente es relevante para la integridad: la confluencia de la prueba es la garantía de que siempre se puede generar un cuadro cerrado a partir de un cuadro arbitrario parcialmente construido (si el conjunto es insatisfactorio). Sin prueba de confluencia, la aplicación de una regla "incorrecta" puede resultar en la imposibilidad de completar el cuadro aplicando otras reglas.
Los cuadros proposicionales y los cuadros sin unificación tienen procedimientos de prueba fuertemente completos. En particular, un procedimiento de prueba completo es el de aplicar las reglas de manera justa . Esto se debe a que la única forma en que tales cálculos no pueden generar un cuadro cerrado a partir de un conjunto insatisfactorio es no aplicando algunas reglas aplicables.
Para los cuadros proposicionales, la equidad equivale a expandir cada fórmula en cada rama. Más precisamente, para cada fórmula y cada rama en la que se encuentra la fórmula, se ha utilizado la regla que tiene la fórmula como condición previa para expandir la rama. Un procedimiento de prueba imparcial para cuadros proposicionales está totalmente completo.
Para cuadros de primer orden sin unificación, la condición de equidad es similar, con la excepción de que la regla para cuantificadores universales podría requerir más de una aplicación. La justicia equivale a expandir cada cuantificador universal con una frecuencia infinita. En otras palabras, una política justa de aplicación de reglas no puede seguir aplicando otras reglas sin expandir de vez en cuando cada cuantificador universal en cada rama que aún esté abierta.
Si un cálculo de cuadro está completo, cada conjunto insatisfactorio de fórmulas tiene un cuadro cerrado asociado. Si bien este cuadro siempre puede obtenerse aplicando algunas de las reglas del cálculo, aún persiste el problema de qué reglas aplicar para una fórmula determinada. Como resultado, la integridad no implica automáticamente la existencia de una política factible de aplicación de reglas que siempre conduzca a un cuadro cerrado para cada conjunto de fórmulas insatisfactorio dado. Si bien un procedimiento de prueba imparcial está completo para el cuadro terrestre y el cuadro sin unificación, este no es el caso para el cuadro con unificación.
Una solución general para este problema es buscar en el espacio de cuadros hasta encontrar uno cerrado (si existe alguno, es decir, el conjunto es insatisfactorio). En este enfoque, se comienza con un cuadro vacío y luego se aplican recursivamente todas las reglas aplicables posibles. Este procedimiento visita un árbol (implícito) cuyos nodos están etiquetados con cuadros, y de manera que el cuadro en un nodo se obtiene del cuadro en su padre aplicando una de las reglas válidas.
Dado que cada rama puede ser infinita, este árbol debe visitarse primero en anchura y no en profundidad. Esto requiere una gran cantidad de espacio, ya que la anchura del árbol puede crecer exponencialmente. Un método que puede visitar algunos nodos más de una vez pero que funciona en el espacio polinomial es visitar primero en profundidad con profundización iterativa : primero se visita la profundidad del árbol hasta una cierta profundidad, luego se aumenta la profundidad y se realiza la visita nuevamente. . Este procedimiento particular utiliza la profundidad (que también es el número de reglas del cuadro que se han aplicado) para decidir cuándo detenerse en cada paso. En su lugar, se han utilizado varios otros parámetros (como el tamaño del cuadro que etiqueta un nodo).
El tamaño del árbol de búsqueda depende del número de cuadros (hijos) que se pueden generar a partir de uno determinado (principal). Por lo tanto, reducir el número de dichos cuadros reduce la búsqueda requerida.
Una forma de reducir este número es no permitir la generación de algunos cuadros basados en su estructura interna. Un ejemplo es la condición de regularidad: si una rama contiene un literal, usar una regla de expansión que genere el mismo literal es inútil porque la rama que contiene dos copias de los literales tendría el mismo conjunto de fórmulas que la original. Esta expansión puede no permitirse porque si existe un cuadro cerrado, se puede encontrar sin él. Esta restricción es estructural porque se puede verificar observando la estructura del cuadro para expandirse únicamente.
Diferentes métodos para reducir la búsqueda no permiten la generación de algunos cuadros basándose en que aún se puede encontrar un cuadro cerrado expandiendo los demás. Estas restricciones se llaman globales. Como ejemplo de restricción global, se puede emplear una regla que especifique cuál de las ramas abiertas se ampliará. Como resultado, si un cuadro tiene, por ejemplo, dos ramas no cerradas, la regla especifica cuál se expandirá, no permitiendo la expansión de la segunda. Esta restricción reduce el espacio de búsqueda porque ahora una posible elección está prohibida; Sin embargo, la integridad no se ve perjudicada, ya que la segunda sucursal aún se ampliará si la primera finalmente se cierra. Como ejemplo, un cuadro con raíz , hijo y dos hojas se puede cerrar de dos maneras: aplicando primero a y luego a , o viceversa. Claramente no hay necesidad de seguir ambas posibilidades; uno puede considerar sólo el caso en el que se aplica por primera vez y descartar el caso en el que se aplica por primera vez . Esta es una restricción global porque lo que permite descuidar esta segunda expansión es la presencia del otro cuadro, donde la expansión se aplica al primero y después.
Cuando se aplican a conjuntos de cláusulas (en lugar de fórmulas arbitrarias), los métodos de cuadros permiten una serie de mejoras de eficiencia. Una cláusula de primer orden es una fórmula que no contiene variables libres y que cada una es literal. Los cuantificadores universales a menudo se omiten por motivos de claridad, de modo que, por ejemplo, en realidad significa . Tenga en cuenta que, si se toman literalmente, estas dos fórmulas no son las mismas que para la satisfacibilidad: más bien, la satisfacibilidad es la misma que la de . El hecho de que las variables libres estén universalmente cuantificadas no es una consecuencia de la definición de satisfacibilidad de primer orden; más bien se utiliza como un supuesto común implícito cuando se trata de cláusulas.
Las únicas reglas de ampliación que son aplicables a una cláusula son y ; estas dos reglas pueden ser reemplazadas por su combinación sin perder su integridad. En particular, la siguiente regla corresponde a aplicar en secuencia las reglas y del cálculo de primer orden con unificación.
Cuando el conjunto cuya satisfacibilidad se va a comprobar está compuesto únicamente por cláusulas, esto y las reglas de unificación son suficientes para demostrar la insatisfacibilidad. En otros mundos, el cuadro de cálculos compuesto por y está completo.
Dado que la regla de expansión de cláusulas solo genera literales y nunca cláusulas nuevas, las cláusulas a las que se puede aplicar son solo cláusulas del conjunto de entrada. Como resultado, la regla de expansión de cláusulas puede restringirse aún más al caso en que la cláusula esté en el conjunto de entrada.
Dado que esta regla explota directamente las cláusulas del conjunto de entrada, no es necesario inicializar el cuadro en la cadena de cláusulas de entrada. Por lo tanto, la tabla inicial se puede inicializar con el nodo único etiquetado ; esta etiqueta a menudo se omite por considerarla implícita. Como resultado de esta mayor simplificación, cada nodo del cuadro (aparte de la raíz) está etiquetado con un literal.
Se pueden utilizar varias optimizaciones para el cuadro de cláusulas. Estas optimizaciones tienen como objetivo reducir la cantidad de cuadros posibles que se explorarán al buscar un cuadro cerrado como se describe en la sección "Búsqueda de un cuadro cerrado" anterior.
La conexión es una condición del cuadro que prohíbe expandir una rama usando cláusulas que no están relacionadas con los literales que ya están en la rama. La conexión se puede definir de dos maneras:
Ambas condiciones se aplican sólo a las ramas que no sólo están formadas por la raíz. La segunda definición permite el uso de una cláusula que contiene un literal que se unifica con la negación de un literal en la rama, mientras que la primera solo restringe aún más que ese literal esté en la hoja de la rama actual.
Si la expansión de la cláusula está restringida por la conexión (ya sea fuerte o débil), su aplicación produce un cuadro en el que se puede aplicar la sustitución a una de las nuevas hojas, cerrando su rama. En particular, esta es la hoja que contiene el literal de la cláusula que se unifica con la negación de un literal en la rama (o la negación del literal en el padre, en caso de una conexión fuerte).
Ambas condiciones de conexión conducen a un cálculo completo de primer orden: si un conjunto de cláusulas es insatisfactorio, tiene un cuadro cerrado y conectado (fuerte o débilmente). Un cuadro cerrado de este tipo se puede encontrar buscando en el espacio de cuadros como se explica en la sección "Búsqueda de un cuadro cerrado". Durante esta búsqueda, la conectividad elimina algunas posibles opciones de expansión, reduciendo así la búsqueda. En otros mundos, si bien el cuadro en un nodo del árbol se puede expandir en general de varias maneras diferentes, la conexión puede permitir solo algunas de ellas, reduciendo así la cantidad de cuadros resultantes que deben expandirse aún más.
Esto se puede ver en el siguiente ejemplo (proposicional). El cuadro formado por una cadena para el conjunto de cláusulas se puede expandir en general usando cada una de las cuatro cláusulas de entrada, pero la conexión solo permite la expansión que usa . Esto significa que el árbol de los cuadros tiene cuatro hojas en general, pero sólo una si se impone la conexión. Esto significa que la conectividad deja sólo un cuadro para intentar ampliar, en lugar de los cuatro que hay que considerar en general. A pesar de esta reducción de opciones, el teorema de completitud implica que se puede encontrar un cuadro cerrado si el conjunto es insatisfactorio.
Las condiciones de conexión, cuando se aplican al caso proposicional (clausal), hacen que el cálculo resultante no sea confluente. Como ejemplo, es insatisfactorio, pero su aplicación genera la cadena , que no está cerrada y a la que no se puede aplicar ninguna otra regla de expansión sin violar la conexión fuerte o débil. En el caso de conectividad débil, la confluencia se cumple siempre que la cláusula utilizada para expandir la raíz sea relevante para la insatisfacibilidad, es decir, esté contenida en un subconjunto mínimamente insatisfactorio del conjunto de cláusulas. Desafortunadamente, el problema de comprobar si una cláusula cumple esta condición es en sí mismo un problema difícil. A pesar de la no confluencia, se puede encontrar un cuadro cerrado mediante la búsqueda, como se presenta en la sección "Búsqueda de un cuadro cerrado" anterior. Si bien la búsqueda se hace necesaria, la conectividad reduce las posibles opciones de expansión, lo que hace que la búsqueda sea más eficiente.
Un cuadro es regular si ningún literal aparece dos veces en la misma rama. Hacer cumplir esta condición permite reducir las posibles opciones de expansión del cuadro, ya que las cláusulas que generarían un cuadro no regular no se pueden ampliar.
Sin embargo, estas medidas de expansión no permitidas son inútiles. Si es una rama que contiene un literal y es una cláusula cuya expansión viola la regularidad, entonces contiene . Para cerrar el cuadro, es necesario expandir y cerrar, entre otras, la rama donde , donde aparece dos veces. Sin embargo, las fórmulas de esta rama son exactamente las mismas que las fórmulas de solo. Como resultado, los mismos pasos de expansión que se cierran también se cierran . Esto significa que la expansión era innecesaria; además, si contenía otros literales, su expansión generaba otras hojas que debían cerrarse. En el caso proposicional, las expansiones necesarias para cerrar estas hojas son completamente inútiles; en el caso de primer orden, es posible que sólo afecten al resto del cuadro debido a algunas unificaciones; Sin embargo, estos se pueden combinar con las sustituciones utilizadas para cerrar el resto del cuadro.
En una lógica modal , un modelo comprende un conjunto de mundos posibles , cada uno asociado a una evaluación de verdad; una relación de accesibilidad especifica cuándo un mundo es accesible desde otro. Una fórmula modal puede especificar no sólo las condiciones de un mundo posible, sino también las que son accesibles desde él. Por ejemplo, es cierto en un mundo si es cierto en todos los mundos a los que se puede acceder desde él.
En cuanto a la lógica proposicional, los cuadros de la lógica modal se basan en dividir fórmulas de forma recursiva en sus componentes básicos. Sin embargo, expandir una fórmula modal puede requerir establecer condiciones en mundos diferentes. Por ejemplo, si es verdadero en un mundo, entonces existe un mundo accesible desde él donde es falso. Sin embargo, no se puede simplemente agregar la siguiente regla a las proposicionales.
En los cuadros proposicionales todas las fórmulas se refieren a la misma evaluación de verdad, pero la condición previa de la regla anterior se cumple en un mundo mientras que la consecuencia se cumple en otro. No tener esto en cuenta generaría resultados incorrectos. Por ejemplo, una fórmula establece que es verdadera en el mundo actual y falsa en un mundo al que se puede acceder desde él. La simple aplicación de y la regla de expansión anterior produciría y , pero estas dos fórmulas en general no deberían generar una contradicción, ya que se mantienen en mundos diferentes. Los cálculos de cuadros modales contienen reglas como la anterior, pero incluyen mecanismos para evitar la interacción incorrecta de fórmulas que se refieren a mundos diferentes.
Técnicamente, los cuadros de lógica modal verifican la satisfacibilidad de un conjunto de fórmulas: verifican si existe un modelo y un mundo tales que las fórmulas del conjunto sean verdaderas en ese modelo y mundo. En el ejemplo anterior, mientras establece la verdad de en , la fórmula establece la verdad de en algún mundo al que se puede acceder y que, en general, puede ser diferente de . Los cálculos de cuadros para lógica modal tienen en cuenta que las fórmulas pueden referirse a mundos diferentes.
Este hecho tiene una consecuencia importante: las fórmulas que se mantienen en un mundo pueden implicar condiciones sobre diferentes sucesores de ese mundo. La insatisfacibilidad puede entonces demostrarse a partir del subconjunto de fórmulas que se refieren a un único sucesor. Esto es válido si un mundo puede tener más de un sucesor, lo cual es cierto para la mayoría de las lógicas modales. Si este es el caso, una fórmula como es verdadera si existe un sucesor donde se mantiene y un sucesor donde se mantiene. A la inversa, si se puede demostrar la insatisfacibilidad de en un sucesor arbitrario, la fórmula resulta insatisfactoria sin comprobar los mundos en los que se cumple. Al mismo tiempo, si uno puede demostrar que no es satisfactorio , no es necesario comprobarlo . Como resultado, si bien hay dos formas posibles de expandir , una de estas dos formas siempre es suficiente para demostrar la insatisfacibilidad si la fórmula es insatisfactoria. Por ejemplo, uno puede ampliar el cuadro considerando un mundo arbitrario donde se cumple. Si esta expansión conduce a la insatisfacibilidad, la fórmula original es insatisfactoria. Sin embargo, también es posible que la insatisfacción no pueda demostrarse de esta manera y que en su lugar se debería haber considerado el mundo en el que se cumple. Como resultado, siempre se puede demostrar la insatisfacción expandiendo solo o solo; sin embargo, si se toma la decisión equivocada, es posible que el cuadro resultante no se cierre. La expansión de cualquiera de las subfórmulas conduce a cálculos de cuadro que son completos pero no confluentes en pruebas. Por lo tanto, puede ser necesario realizar una búsqueda como se describe en "Búsqueda de un cuadro cerrado".
Dependiendo de si la condición previa y la consecuencia de una regla de expansión del cuadro se refieren al mismo mundo o no, la regla se llama estática o transaccional. Si bien las reglas para los conectivos proposicionales son todas estáticas, no todas las reglas para los conectivos modales son transaccionales: por ejemplo, en toda lógica modal, incluido el axioma T , se cumple que implica en el mismo mundo. Como resultado, la regla de expansión relativa (modal) del cuadro es estática, ya que tanto su condición previa como su consecuencia se refieren al mismo mundo.
Un método para evitar que las fórmulas que hacen referencia a mundos diferentes interactúen de manera incorrecta es asegurarse de que todas las fórmulas de una rama se refieran al mismo mundo. Esta condición es inicialmente cierta ya que se supone que todas las fórmulas del conjunto cuya coherencia se debe verificar se refieren al mismo mundo. Al expandir una rama, son posibles dos situaciones: o las nuevas fórmulas se refieren al mismo mundo que el otro en la rama o no. En el primer caso, la regla se aplica normalmente. En el segundo caso, todas las fórmulas de la rama que no se aplican también en el nuevo mundo se eliminan de la rama y posiblemente se agregan a todas las demás ramas que todavía son relativas al viejo mundo.
Como ejemplo, en S5 cada fórmula que es verdadera en un mundo también lo es en todos los mundos accesibles (es decir, en todos los mundos accesibles tanto y son verdaderas). Por lo tanto, al aplicar , cuya consecuencia se cumple en un mundo diferente, se eliminan todas las fórmulas de la rama, pero se pueden conservar todas las fórmulas , ya que también se aplican en el nuevo mundo. Para mantener la integridad, las fórmulas eliminadas se agregan a todas las demás ramas que todavía hacen referencia al viejo mundo.
Un mecanismo diferente para garantizar la interacción correcta entre fórmulas que se refieren a mundos diferentes es cambiar de fórmulas a fórmulas etiquetadas: en lugar de escribir , se escribiría para dejar explícito lo que se cumple en el mundo .
Todas las reglas de expansión proposicional se adaptan a esta variante afirmando que todas se refieren a fórmulas con la misma etiqueta mundial. Por ejemplo, genera dos nodos etiquetados con y ; una rama se cierra sólo si contiene dos literales opuestos del mismo mundo, como y ; no se genera ningún cierre si las dos etiquetas mundiales son diferentes, como en y .
Una regla de expansión modal puede tener una consecuencia que se refiera a mundos diferentes. Por ejemplo, la regla para se escribiría de la siguiente manera
La condición previa y consecuente de esta regla se refieren a mundos y , respectivamente. Los distintos cálculos utilizan diferentes métodos para realizar un seguimiento de la accesibilidad de los mundos utilizados como etiquetas. Algunas incluyen pseudofórmulas como para indicar que se puede acceder desde . Algunos otros usan secuencias de números enteros como etiquetas mundiales, y esta notación representa implícitamente la relación de accesibilidad (por ejemplo, es accesible desde .)
El problema de la interacción entre fórmulas que se mantienen en mundos diferentes se puede superar mediante el uso de cuadros de etiquetado de conjuntos. Son árboles cuyos nodos están etiquetados con conjuntos de fórmulas; las reglas de expansión explican cómo adjuntar nuevos nodos a una hoja, basándose únicamente en la etiqueta de la hoja (y no en la etiqueta de otros nodos de la rama).
Los cuadros para lógica modal se utilizan para verificar la satisfacibilidad de un conjunto de fórmulas modales en una lógica modal determinada. Dado un conjunto de fórmulas , comprueban la existencia de un modelo y un mundo tal que .
Las reglas de expansión dependen de la lógica modal particular utilizada. Se puede obtener un sistema de cuadro para la lógica modal básica K agregando a las reglas del cuadro proposicional la siguiente:
Intuitivamente, la condición previa de esta regla expresa la verdad de todas las fórmulas en todos los mundos accesibles, y la verdad de algunos mundos accesibles. La consecuencia de esta regla es una fórmula que debe ser verdadera en uno de esos mundos donde lo es.
Más técnicamente, los métodos de cuadros modales verifican la existencia de un modelo y un mundo que hacen verdadero un conjunto de fórmulas. Si son verdaderas en , debe haber un mundo que sea accesible desde y que las haga verdaderas. Por lo tanto, esta regla equivale a derivar un conjunto de fórmulas que deben cumplirse en tales casos .
Si bien las condiciones previas se suponen satisfechas por , las consecuencias se suponen satisfechas en : el mismo modelo pero posiblemente en mundos diferentes. Los cuadros etiquetados por conjuntos no realizan un seguimiento explícito del mundo donde cada fórmula se supone verdadera: dos nodos pueden referirse o no al mismo mundo. Sin embargo, las fórmulas que etiquetan cualquier nodo determinado se supone que son verdaderas en el mismo mundo.
Como resultado de los mundos posiblemente diferentes donde las fórmulas se suponen verdaderas, una fórmula en un nodo no es automáticamente válida en todos sus descendientes, ya que cada aplicación de la regla modal corresponde a un movimiento de un mundo a otro. Esta condición se captura automáticamente mediante cuadros de etiquetado de conjuntos, ya que las reglas de expansión se basan únicamente en la hoja donde se aplican y no en sus ancestros.
En particular, no se extiende directamente a múltiples fórmulas en cuadros negados como en : si bien existe un mundo accesible donde es falso y otro en el que es falso, estos dos mundos no son necesariamente iguales.
A diferencia de las reglas proposicionales, establece condiciones sobre todas sus precondiciones. Por ejemplo, no se puede aplicar a un nodo etiquetado con ; Si bien este conjunto es inconsistente y esto podría probarse fácilmente aplicando , esta regla no se puede aplicar debido a la fórmula , que ni siquiera es relevante para la inconsistencia. La eliminación de tales fórmulas es posible gracias a la regla:
La adición de esta regla (regla de adelgazamiento) hace que el cálculo resultante no sea confluente: puede ser imposible cerrar un cuadro para un conjunto inconsistente, incluso si existe un cuadro cerrado para el mismo conjunto.
La regla no es determinista: el conjunto de fórmulas que se eliminarán (o se mantendrán) se puede elegir arbitrariamente; esto crea el problema de elegir un conjunto de fórmulas para descartar que no sea tan grande que haga que el conjunto resultante sea satisfactorio y no tan pequeño que haga que las reglas de expansión necesarias sean inaplicables. Tener un gran número de opciones posibles dificulta el problema de buscar un cuadro cerrado.
Este no determinismo puede evitarse restringiendo el uso de de modo que sólo se aplique antes de una regla de expansión modal y de modo que sólo elimine las fórmulas que hacen que esa otra regla sea inaplicable. Esta condición también puede formularse fusionando las dos reglas en una sola. La regla resultante produce el mismo resultado que la anterior, pero implícitamente descarta todas las fórmulas que hicieron que la regla anterior fuera inaplicable. Se ha demostrado que este mecanismo de eliminación preserva la integridad de muchas lógicas modales.
El axioma T expresa la reflexividad de la relación de accesibilidad: cada mundo es accesible desde sí mismo. La regla de expansión del cuadro correspondiente es:
Esta regla relaciona condiciones sobre un mismo mundo: si es cierta en un mundo, por reflexividad también lo es en el mismo mundo . Esta regla es estática, no transaccional, ya que tanto su condición previa como su consecuente se refieren al mismo mundo.
Esta regla copia de la condición previa al consecuente, a pesar de que esta fórmula haya sido "utilizada" para generar . Esto es correcto, así como el mundo considerado es el mismo, también se cumple allí. Esta "copia" es necesaria en algunos casos. Es necesario, por ejemplo, demostrar la inconsistencia de : las únicas reglas aplicables están en orden , de las cuales se bloquea si no se copia.
Un método diferente para tratar con fórmulas que se mantienen en mundos alternativos es comenzar un cuadro diferente para cada mundo nuevo que se introduce en el cuadro. Por ejemplo, implica que es falso en un mundo accesible, por lo que se inicia un nuevo cuadro con raíz en . Este nuevo cuadro se adjunta al nodo del cuadro original donde se aplicó la regla de expansión; un cierre de este cuadro genera inmediatamente un cierre de todas las ramas donde se encuentra ese nodo, independientemente de si el mismo nodo está asociado a otros cuadros auxiliares. Las reglas de expansión para los cuadros auxiliares son las mismas que para el original; por lo tanto, un cuadro auxiliar puede tener a su vez otros cuadros (sub)auxiliares.
Los cuadros modales anteriores establecen la coherencia de un conjunto de fórmulas y pueden usarse para resolver el problema de consecuencias lógicas locales . Este es el problema de decir si, para cada modelo , si es cierto en un mundo , entonces también lo es en el mismo mundo. Esto es lo mismo que comprobar si es cierto en un mundo de un modelo, suponiendo que también es cierto en el mismo mundo del mismo modelo.
Un problema relacionado es el problema de las consecuencias globales, donde se supone que una fórmula (o un conjunto de fórmulas) es verdadera en todos los mundos posibles del modelo. El problema es comprobar si, en todos los modelos, lo que es cierto en todos los mundos, también lo es en todos los mundos.
Los supuestos locales y globales difieren en los modelos en los que la fórmula supuesta es cierta en algunos mundos pero no en otros. Por ejemplo, implica globalmente pero no localmente. La vinculación local no se sostiene en un modelo que consta de dos mundos que hacen y son verdaderos, respectivamente, y donde el segundo es accesible desde el primero; En el primer mundo, las suposiciones son ciertas pero son falsas. Este contraejemplo funciona porque se puede asumir que es verdadero en un mundo y falso en otro. Sin embargo, si el mismo supuesto se considera global, no está permitido en ningún mundo del modelo.
Estos dos problemas se pueden combinar, de modo que se pueda comprobar si se trata de una consecuencia local del supuesto global . Los cálculos de Tableaux pueden abordar el supuesto global mediante una regla que permite su adición a cada nodo, independientemente del mundo al que se refiere.
A veces se utilizan las siguientes convenciones.
Al escribir reglas de expansión de cuadros, las fórmulas a menudo se denotan mediante una convención, de modo que, por ejemplo, siempre se considera . La siguiente tabla proporciona la notación de fórmulas en lógica proposicional, de primer orden y modal.
Cada etiqueta de la primera columna se considera cualquiera de las fórmulas de las otras columnas. Una fórmula sobrerayada como indica que es la negación de cualquier fórmula que aparezca en su lugar, de modo que, por ejemplo, en la fórmula la subfórmula es la negación de .
Dado que cada etiqueta indica muchas fórmulas equivalentes, esta notación permite escribir una única regla para todas estas fórmulas equivalentes. Por ejemplo, la regla de expansión de la conjunción se formula como:
Una fórmula en un cuadro se supone verdadera. Los cuadros firmados permiten afirmar que una fórmula es falsa. Esto generalmente se logra agregando una etiqueta a cada fórmula, donde la etiqueta T indica las fórmulas que se suponen verdaderas y F las que se suponen falsas. Una notación diferente pero equivalente es la de escribir fórmulas que se suponen verdaderas a la izquierda del nodo y fórmulas que se suponen falsas a su derecha.
