En teoría de la prueba , el cuadro semántico [1] ( / t æ ˈ b l oʊ , ˈ t æ b l oʊ / ; plural: tableaux ), también llamado cuadro analítico , [2] árbol de verdad , [1] o simplemente árbol , [2] 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 . [1] 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. El cálculo construye este árbol y lo usa para probar o refutar la fórmula completa. [3] 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 . [4]
Un método de árboles de verdad contiene un conjunto fijo de reglas para producir árboles a partir de una fórmula lógica dada, o un conjunto de fórmulas lógicas. Esos árboles tendrán más fórmulas en cada rama, y en algunos casos, una rama puede llegar a contener tanto una fórmula como su negación, es decir, una contradicción. En ese caso, se dice que la rama se cierra . [1] Si cada rama de un árbol se cierra, se dice que el árbol mismo se cierra. En virtud de las reglas para la construcción de tablas, un árbol cerrado es una prueba de que la fórmula original, o el conjunto de fórmulas, utilizado para construirlo era en sí mismo autocontradictorio, [1] y por lo tanto falso. A la inversa, una tabla también puede probar que una fórmula lógica es tautóloga : si una fórmula es tautóloga, su negación es una contradicción, por lo que una tabla construida a partir de su negación se cerrará. [1]
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. [5]
El método de los cuadros semánticos fue inventado por el lógico holandés Evert Willem Beth (Beth 1955) [6] y simplificado, para la lógica clásica, por Raymond Smullyan (Smullyan 1968, 1995). [7] La simplificación de Smullyan, "cuadros unilaterales", se describe aquí. El método de Smullyan ha sido generalizado a lógicas proposicionales y de primer orden arbitrarias de múltiples valores por Walter Carnielli (Carnielli 1987). [8]
Los cuadros pueden verse intuitivamente como sistemas secuenciales invertidos. Esta relación simétrica entre cuadros y sistemas secuenciales se estableció formalmente en (Carnielli 1991). [9]
Una fórmula en lógica proposicional consta de letras que representan proposiciones y conectores para conjunción , disyunción , condicionales , bicondicionales y negación . La verdad o falsedad de una proposición se denomina valor de verdad. Se dice que una fórmula, o un conjunto de fórmulas, es satisfacible si existe una posible asignación de valores de verdad a las letras proposicionales de modo que la fórmula completa, que combina las letras con conectores, sea también verdadera. [1] Se dice que tal asignación satisface la fórmula. [2]
Una tabla comprueba si un conjunto dado de fórmulas es satisfacible o no. Puede utilizarse para comprobar tanto la validez como la implicación: una fórmula es válida si su negación es insatisfacible y las fórmulas implican si es insatisfacible.
La siguiente tabla muestra algunas variantes de notación para los conectores lógicos, para los lectores que pueden estar más familiarizados con una notación diferente a la que se utiliza aquí. En general, al momento de la inclusión de esta oración, se ha utilizado el primer símbolo de cada línea en el texto de este artículo; sin embargo, dado que los editores de Wikipedia no están obligados a utilizar una notación consistente dentro de los artículos o entre ellos, esto puede cambiar.
El principio principal 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 sobre 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 la adición 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 insatisfacbilidad. [12] Luego, el siguiente procedimiento puede aplicarse repetidamente de forma no determinista:
Eventualmente, este procedimiento finalizará, porque en algún momento se aplicará cada nodo aplicable 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 de la tabla es que las fórmulas en los nodos de la misma rama se consideran en conjunto, mientras que las diferentes ramas se consideran disyuntivas. Como resultado, una tabla 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 la tabla de tal manera que la fórmula representada por la tabla 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 insatisfacible. Si se demuestra que todas las conjunciones son insatisfacibles, el conjunto original de fórmulas es insatisfacible.
Siempre que una rama de una tabla contiene una fórmula que es la conjunción de dos fórmulas, estas dos fórmulas son consecuencias de esa fórmula. Este hecho se puede formalizar mediante la siguiente regla para la expansión de una tabla:
( ) Si una rama de la tabla 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 puede agregar al final de una rama que contenga . Más precisamente, si un nodo de una rama está etiquetado como , se puede agregar a la rama la nueva hoja .
Si una rama de una tabla 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 crea dos hijos hermanos de la hoja de la rama, que contengan las fórmulas y , respectivamente.
Esta regla divide una rama en dos, diferenciándose únicamente en el nodo final. Dado que las ramas se consideran disyuntivas 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 se escribe formalmente generalmente utilizando el símbolo para separar las fórmulas de los dos nodos distintos que se van a crear:
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 como y , respectivamente.
El objetivo de las tablas 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 literales. Alternativamente, se pueden usar las leyes de De Morgan durante la expansión de la tabla, de modo que por ejemplo se trate como . Las reglas que introducen o eliminan un par de negaciones (como en ) también se usan en este caso (de lo contrario, no habría forma de expandir una fórmula como :
Cada tabla puede considerarse como una representación gráfica de una fórmula, que es equivalente al conjunto a partir del cual se construye la tabla. Esta fórmula es la siguiente: cada rama de la tabla representa la conjunción de sus fórmulas; la tabla representa la disyunción de sus ramas. Las reglas de expansión transforman una tabla en una que tiene una fórmula representada equivalente. Dado que la tabla se inicializa como una sola rama que contiene las fórmulas del conjunto de entrada, todas las tablas posteriores obtenidas a partir de ella representan fórmulas que son equivalentes a ese conjunto (en la variante donde la tabla inicial es el nodo único etiquetado como verdadero, las fórmulas representadas por las tablas son consecuencias del conjunto original).
El método de tablas funciona partiendo del conjunto inicial de fórmulas y luego añadiendo a la tabla fórmulas cada vez más simples hasta que se muestre la contradicción en la forma simple de literales opuestos. Dado que la fórmula representada por una tabla 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 insatisfacible. Como resultado, esta rama ahora puede "cerrarse", ya que no hay necesidad de expandirla más. Si todas las ramas de una tabla están cerradas, la fórmula representada por la tabla es insatisfacible; por lo tanto, el conjunto original también es insatisfacible. Obtener una tabla donde todas las ramas estén cerradas es una forma de probar la insatisfacibilidad del conjunto original. En el caso proposicional, también se puede probar que la satisfacibilidad se prueba por la imposibilidad de encontrar una tabla cerrada, siempre que cada regla de expansión se haya aplicado en todos los lugares donde podría aplicarse. En particular, si una tabla contiene algunas ramas abiertas (no cerradas) y cada fórmula que no es un 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 satisfacible.
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 ramificación "debajo" del nodo). En este caso, la regla para expandir la fórmula debe aplicarse de modo que su(s) conclusión(es) se añadan a todas estas ramas que aún están abiertas, antes de que se pueda concluir que la tabla no se puede expandir más y que, por lo tanto, la fórmula es satisfacible.
Una variante de la tabla es etiquetar los nodos con conjuntos de fórmulas en lugar de fórmulas individuales. En este caso, la tabla inicial es un nodo único etiquetado con el conjunto que se debe demostrar que es satisfacible. Por lo tanto, se considera que las fórmulas de un conjunto están en conjunción.
Las reglas de expansión de la tabla ahora pueden funcionar en las hojas de la tabla, 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:
Una tabla para un conjunto finito X dado es un árbol finito (al revés) con raíz X en el que todos los nodos secundarios se obtienen aplicando las reglas de la tabla a sus nodos primarios. Una rama en una tabla de este tipo está cerrada si su nodo de hoja contiene "cerrado". Una tabla está cerrada si todas sus ramas están cerradas. Una tabla está abierta si al menos una rama no está cerrada.
A continuación se muestran dos cuadros cerrados para el conjunto.
Cada aplicación de la regla está marcada en el lado derecho. Ambas logran el mismo efecto, la primera cierra más rápido. La única diferencia es el orden en el que se realiza la reducción.
y el segundo, más largo, con las reglas aplicadas en un orden diferente:
La primera tabla se cierra después de una sola aplicación de la regla, mientras que la segunda no da en el blanco y tarda mucho más en cerrarse. Claramente, preferiríamos encontrar siempre las tablas cerradas más cortas, pero se puede demostrar que no puede existir un único algoritmo que encuentre las tablas cerradas más cortas para todos los conjuntos de fórmulas de entrada. [ cita requerida ]
Las tres reglas , y dadas anteriormente son suficientes para decidir si un conjunto dado de fórmulas en forma normal negada son conjuntamente satisfactorias:
Simplemente apliquemos 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 todo cuadro para es abierto.
En el primer caso, es conjuntamente insatisfacible y en el segundo caso, 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 la hace conjuntamente satisfacible. La lógica clásica tiene en realidad la propiedad bastante agradable de que necesitamos investigar solo (cualquier) tabla completa: si es cerrada, entonces es insatisfacible y si es abierta, entonces es satisfacible. Pero esta propiedad no la disfrutan generalmente otras lógicas.
Estas reglas son suficientes para toda la lógica clásica tomando un conjunto inicial de fórmulas X y reemplazando cada miembro C por su forma normal negada lógicamente equivalente C', lo que da un conjunto de fórmulas X' . Sabemos que X es satisfacible si y solo si X' es satisfacible, por lo que basta con buscar una tabla cerrada para X' utilizando el procedimiento descrito anteriormente.
Mediante el planteamiento podemos comprobar si la fórmula A es una tautología de la lógica clásica:
Si la tabla para se cierra, entonces es insatisfacible y, por lo tanto, A es una tautología, ya que ninguna asignación de valores de verdad hará que A sea falsa . De lo contrario, cualquier hoja abierta de cualquier rama abierta de cualquier tabla abierta para da una asignación que falsifica A.
La lógica proposicional clásica suele tener un conectivo para denotar la implicación material . Si escribimos este conectivo como ⇒, entonces la fórmula A ⇒ B significa "si A entonces B ". Es posible dar una regla de tabla 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 darían un procedimiento de terminación para decidir si un conjunto dado de fórmulas es simultáneamente satisfacible 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 solo á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 cumplen 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 por los lados derechos en C , entonces obtendremos una fórmula C' que es lógicamente equivalente a C pero que tiene la propiedad de que C' no contiene implicaciones y ¬ aparece solo delante de fórmulas atómicas. Se dice que una fórmula de este tipo está en forma normal de negación y es posible demostrar formalmente que cada fórmula C de lógica clásica tiene una fórmula lógicamente equivalente C' en forma normal de negación. Es decir, C es satisfacible si y solo si C' es satisfacible.
Las reglas anteriores para la tabla proposicional se pueden simplificar utilizando la notación uniforme. En la 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 . Las fórmulas de tipo alfa se pueden considerar conjuntivas, ya que tanto y están implícitas por ser verdaderas. Las fórmulas de tipo beta se pueden considerar disyuntivas, ya que tanto o como están implícitas por ser verdaderas. Las siguientes tablas muestran cómo determinar el tipo y los componentes de cualquier fórmula proposicional dada:
En cada tabla, la columna situada más a la izquierda muestra todas las estructuras posibles para las fórmulas de tipo alfa o beta, y las columnas situadas más a la derecha muestran sus respectivos componentes. Alternativamente, las reglas para la notación uniforme pueden expresarse mediante fórmulas con signo:
Al construir una tabla proposicional utilizando la notación anterior, siempre que se encuentre una fórmula de tipo alfa, sus dos componentes se agregan a la rama actual que se está expandiendo. Siempre que se encuentre una fórmula de tipo beta en alguna rama , se puede dividir en dos ramas, una con el conjunto { , } de fórmulas y la otra con el conjunto { , } de fórmulas. [14]
Las tablas 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 tratar los cuantificadores existenciales, pero difieren en el tratamiento de los cuantificadores universales.
Se supone aquí 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 universalmente de manera implícita, 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 es un término fundamental . Por lo tanto, la siguiente regla de inferencia es correcta:
A diferencia de las reglas para los conectivos proposicionales, pueden ser necesarias múltiples aplicaciones de esta regla a la misma fórmula. Por ejemplo, el conjunto solo puede demostrarse insatisfactorio si tanto y se generan a partir de .
Los cuantificadores existenciales se tratan mediante la eskolemización. En particular, una fórmula con un cuantificador existencial principal como genera su eskolemización , donde es un nuevo símbolo constante.
El término de Skolem es una constante (una función de aridad 0) porque la cuantificación sobre no ocurre dentro del alcance de ningún cuantificador universal. Si la fórmula original contenía algunos cuantificadores universales tales que la cuantificación sobre estaba dentro de su alcance, estos cuantificadores evidentemente han sido eliminados por la aplicación de la regla para cuantificadores universales.
La regla de cuantificadores existenciales introduce nuevos símbolos constantes. Estos símbolos pueden ser utilizados por la regla de cuantificadores universales, de modo que se puede generar incluso si no estaba en la fórmula original sino que es una constante de Skolem creada por la regla de cuantificadores existenciales.
Las dos reglas anteriores para cuantificadores universales y existenciales son correctas, y también lo son las reglas proposicionales: si un conjunto de fórmulas genera una tabla cerrada, este conjunto es insatisfacible. La completitud también puede probarse: si un conjunto de fórmulas es insatisfacible, existe una tabla cerrada construida a partir de él mediante estas reglas. Sin embargo, encontrar realmente dicha tabla cerrada requiere una política adecuada de aplicación de reglas. De lo contrario, un conjunto insatisfacible puede generar una tabla de crecimiento infinito. A modo de ejemplo, el conjunto es insatisfacible, pero nunca se obtiene una tabla cerrada si uno sigue aplicando imprudentemente la regla para cuantificadores universales a , generando, por ejemplo , . Siempre se puede encontrar una tabla cerrada descartando esta y otras políticas "injustas" similares de aplicación de reglas de tabla.
La regla para cuantificadores universales es la única regla no determinista, ya que no especifica con qué término se debe crear la instancia. Además, mientras que las otras reglas deben aplicarse solo una vez para cada fórmula y cada ruta en la que se encuentre la fórmula, esta puede requerir múltiples aplicaciones. Sin embargo, la aplicación de esta regla se puede restringir retrasando la aplicación de la regla hasta que no sea aplicable ninguna otra regla y restringiendo la aplicación de la regla a los términos básicos que ya aparecen en la ruta de la tabla. La variante de las tablas con unificación que se muestra a continuación tiene como objetivo resolver el problema del no determinismo.
El principal problema de una tabla sin unificación es cómo elegir un término básico para la regla del cuantificador universal. De hecho, se pueden utilizar todos los términos básicos posibles, pero es evidente que la mayoría de ellos podrían resultar inútiles para cerrar la tabla.
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 de la tabla. Esto se puede hacer utilizando una variable en lugar de un término, de modo que genere , y luego permitiendo sustituciones para reemplazar posteriormente con un término. La regla para cuantificadores universales se convierte en:
Si bien se supone que el conjunto inicial de fórmulas no contiene variables libres, una fórmula de la tabla 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 de la tabla, solucionando así el problema de generar términos que podrían ser inútiles.
A modo de 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 con ; aplicar esta sustitución da como resultado reemplazar con , que cierra la tabla.
Esta regla cierra al menos una rama de la tabla (la que contiene el par de literales considerado). Sin embargo, la sustitución debe aplicarse a toda la tabla, no solo a estos dos literales. Esto se expresa diciendo que las variables libres de la tabla son rígidas : si una ocurrencia de una variable se reemplaza por otra, todas las demás ocurrencias de la misma variable deben reemplazarse de la misma manera. Formalmente, las variables libres están cuantificadas universalmente (implícitamente) y todas las fórmulas de la tabla están dentro del alcance de estos cuantificadores.
Los cuantificadores existenciales se tratan mediante la eskolemización. A diferencia de la tabla sin unificación, los términos de Skolem no pueden ser constantes simples. De hecho, las fórmulas en una tabla con unificación pueden contener variables libres, que implícitamente se consideran cuantificadas universalmente. Como resultado, una fórmula como puede estar dentro del alcance de los cuantificadores universales; si este es el caso, el término de Skolem no es una constante simple 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 con respecto a una regla donde las variables libres son de la rama, no de una sola. Esta regla se puede simplificar aún más mediante la reutilización de un símbolo de función si ya se ha utilizado en una fórmula que es idéntica a la de hasta el cambio de nombre de la variable.
La fórmula representada por una tabla se obtiene de una manera similar al caso proposicional, con el supuesto adicional de que las variables libres se consideran cuantificadas universalmente. En cuanto al caso proposicional, las fórmulas en cada rama están unidas y las fórmulas resultantes están disjuntas. 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 es la fórmula obtenida disjuntando la conjunción de las fórmulas en cada rama, y son las variables libres en ella, entonces es la fórmula representada por la tabla. Se aplican las siguientes consideraciones:
Las dos variantes siguientes también son correctas.
Las tablas con unificación pueden demostrarse completas: si un conjunto de fórmulas es insatisfactorio, existe una prueba de tabla con unificación. Sin embargo, encontrar una prueba de este tipo puede ser un problema difícil. A diferencia del caso sin unificación, la aplicación de una sustitución puede modificar la parte existente de una tabla; si bien la aplicación de una sustitución cierra al menos una rama, puede hacer que otras ramas sean imposibles de cerrar (incluso si el conjunto es insatisfactorio).
Una solución a este problema es la instanciación diferida : no se aplica ninguna sustitución hasta que se encuentra una que cierra todas las ramas al mismo tiempo. Con esta variante, siempre se puede encontrar una prueba de 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 memoria: el método general cierra las ramas, que luego se pueden descartar, mientras que esta variante no cierra ninguna rama hasta el final.
El problema de que algunas tablas que se pueden generar son imposibles de cerrar incluso si el conjunto es insatisfactorio es común a otros conjuntos de reglas de expansión de tablas: incluso si algunas secuencias específicas de aplicación de estas reglas permiten construir una tabla cerrada (si el conjunto es insatisfactorio), otras secuencias conducen a tablas que no se pueden cerrar. Las soluciones generales para estos casos se describen en la sección "Búsqueda de una tabla".
Un cálculo de tabla es un conjunto de reglas que permiten construir y modificar una tabla. Las reglas de tabla proposicionales, las reglas de tabla sin unificación y las reglas de tabla con unificación son todas cálculos de tabla. Algunas propiedades importantes que un cálculo de tabla puede o no poseer son la completitud, la destructividad y la confluencia de pruebas.
Un cálculo de tablas se considera completo si permite construir una demostración de tablas para cada conjunto insatisfactorio de fórmulas. Los cálculos de tablas 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 añadiéndole nuevos nodos, mientras que el primero permite realizar sustituciones para modificar la parte existente del cuadro. En términos más generales, los cálculos de cuadro se clasifican como destructivos o no destructivos según solo añadan nuevos nodos al cuadro o no. Por tanto, el cuadro con unificación es destructivo, mientras que el cuadro proposicional y el cuadro sin unificación son no destructivos.
La confluencia de pruebas es la propiedad de un cálculo de tablas que permite obtener una prueba para un conjunto insatisfactorio arbitrario a partir de una tabla arbitraria, suponiendo que esta tabla se ha obtenido aplicando las reglas del cálculo. En otras palabras, en un cálculo de tablas confluente de pruebas, a partir de un conjunto insatisfactorio se puede aplicar cualquier conjunto de reglas y aun así obtener una tabla a partir de la cual se puede obtener una tabla cerrada aplicando algunas otras reglas.
Un cálculo de tabla es simplemente un conjunto de reglas que prescribe cómo se puede modificar una tabla. Un procedimiento de prueba es un método para encontrar una prueba (si existe una). En otras palabras, un cálculo de tabla 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 las reglas conducen a una prueba de un conjunto insatisfactorio. Por ejemplo, es insatisfactorio, pero tanto las tablas con unificación como las tablas sin unificación permiten que la regla para los cuantificadores universales se aplique repetidamente a la última fórmula, mientras que la simple aplicación de la regla para la 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 una tabla cerrada para cualquier conjunto insatisfactorio de fórmulas. La confluencia de prueba del cálculo subyacente es relevante para la completitud: la confluencia de prueba es la garantía de que siempre se puede generar una tabla cerrada a partir de una tabla parcialmente construida arbitrariamente (si el conjunto es insatisfactorio). Sin la confluencia de prueba, la aplicación de una regla "incorrecta" puede dar como resultado la imposibilidad de hacer que la tabla sea completa aplicando otras reglas.
Los cuadros proposicionales y los cuadros sin unificación tienen procedimientos de prueba muy 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.
En el caso de los cuadros proposicionales, la imparcialidad consiste en 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 es fuertemente completo.
En el caso de tablas de primer orden sin unificación, la condición de imparcialidad es similar, con la excepción de que la regla para cuantificadores universales podría requerir más de una aplicación. La imparcialidad equivale a expandir cada cuantificador universal infinitamente a menudo. En otras palabras, una política justa de aplicación de reglas no puede seguir aplicando otras reglas sin expandir cada cuantificador universal en cada rama que aún esté abierta de vez en cuando.
Si un cálculo de tabla es completo, cada conjunto insatisfactorio de fórmulas tiene una tabla cerrada asociada. Si bien esta tabla siempre se puede obtener aplicando algunas de las reglas del cálculo, el problema de qué reglas aplicar para una fórmula dada aún persiste. Como resultado, la completitud no implica automáticamente la existencia de una política factible de aplicación de reglas que siempre conduzca a una tabla cerrada para cada conjunto insatisfactorio de fórmulas. Si bien un procedimiento de prueba justo es completo para la tabla básica y la tabla sin unificación, este no es el caso para la tabla con unificación.
Una solución general para este problema es la de buscar en el espacio de tablas hasta encontrar una cerrada (si existe alguna, es decir, el conjunto es insatisfacible). En este enfoque, se comienza con una tabla vacía y luego se aplican recursivamente todas las reglas posibles aplicables. Este procedimiento visita un árbol (implícito) cuyos nodos están etiquetados con tablas, y de modo que la tabla en un nodo se obtiene a partir de la tabla en su padre aplicando una de las reglas válidas.
Dado que cada rama puede ser infinita, este árbol debe visitarse primero en amplitud en lugar de primero en profundidad. Esto requiere una gran cantidad de espacio, ya que la amplitud 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 el árbol en profundidad hasta una cierta profundidad, luego se aumenta la profundidad y se realiza la visita nuevamente. Este procedimiento en particular utiliza la profundidad (que también es la cantidad de reglas de tabla 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 de la tabla que etiqueta un nodo).
El tamaño del árbol de búsqueda depende de la cantidad de tablas (hijas) que se pueden generar a partir de una tabla (principal) dada. Por lo tanto, al reducir la cantidad de dichas tablas se reduce la búsqueda requerida.
Una forma de reducir este número es no permitir la generación de algunas tablas en función de su estructura interna. Un ejemplo es la condición de regularidad: si una rama contiene un literal, utilizar 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 se puede rechazar porque si existe una tabla cerrada, se puede encontrar sin ella. Esta restricción es estructural porque se puede comprobar observando la estructura de la tabla para expandirla únicamente.
Diferentes métodos para reducir la búsqueda no permiten la generación de algunos cuadros con el argumento de que un cuadro cerrado todavía se puede encontrar expandiendo los otros. Estas restricciones se denominan globales. Como ejemplo de una restricción global, se puede emplear una regla que especifique cuál de las ramas abiertas se va a expandir. Como resultado, si un cuadro tiene, por ejemplo, dos ramas no cerradas, la regla especifica cuál se va a expandir, lo que no permite la expansión de la segunda. Esta restricción reduce el espacio de búsqueda porque ahora se prohíbe una opción posible; sin embargo, la completitud no se ve perjudicada, ya que la segunda rama se expandirá de todos modos si finalmente se cierra la primera. Como ejemplo, un cuadro con raíz , hijo y dos hojas y se puede cerrar de dos maneras: aplicando primero a y luego a , o viceversa. Claramente no hay necesidad de seguir ambas posibilidades; se puede considerar solo el caso en el que se aplica primero a e ignorar el caso en el que se aplica primero a . Esta es una restricción global porque lo que permite descuidar esta segunda expansión es la presencia de la otra tabla, donde la expansión se aplica primero y después.
Cuando se aplican a conjuntos de cláusulas (en lugar de fórmulas arbitrarias), los métodos de tablas permiten una serie de mejoras de eficiencia. Una cláusula de primer orden es una fórmula que no contiene variables libres y tal que cada una es un literal. Los cuantificadores universales se omiten a menudo para mayor 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 . Que las variables libres estén cuantificadas universalmente 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 expansión que son aplicables a una cláusula son y ; estas dos reglas pueden ser reemplazadas por su combinación sin perder completitud. 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 desea comprobar está compuesto únicamente de cláusulas, esta regla y las reglas de unificación son suficientes para demostrar la insatisfacibilidad. En otras palabras, el cuadro de cálculos compuesto de 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 se puede restringir aún más al caso en que la cláusula se encuentre en el conjunto de entrada.
Dado que esta regla explota directamente las cláusulas del conjunto de entrada, no es necesario inicializar la tabla con la cadena de cláusulas de entrada. Por lo tanto, la tabla inicial se puede inicializar con el nodo único etiquetado ; esta etiqueta se omite a menudo por ser implícita. Como resultado de esta simplificación adicional, cada nodo de la tabla (excepto la raíz) se etiqueta con un literal.
Se pueden utilizar varias optimizaciones para las tablas de cláusulas. Estas optimizaciones tienen como objetivo reducir la cantidad de tablas posibles que se pueden explorar al buscar una tabla cerrada, como se describe en la sección "Búsqueda de una tabla cerrada" anterior.
La conexión es una condición de Tableau que prohíbe expandir una rama utilizando 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 únicamente a ramas que no constan únicamente de 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 limita aún más que el literal se encuentre en la hoja de la rama actual.
Si la expansión de la cláusula está restringida por la conectividad (ya sea fuerte o débil), su aplicación produce una tabla en la que se puede aplicar la sustitución a una de las nuevas hojas, cerrando su rama. En particular, se trata de 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 conectividad conducen a un cálculo de primer orden completo: si un conjunto de cláusulas es insatisfactorio, tiene una tabla cerrada conectada (fuerte o débilmente). Dicha tabla cerrada se puede encontrar buscando en el espacio de tablas como se explica en la sección "Búsqueda de una tabla cerrada". Durante esta búsqueda, la conectividad elimina algunas posibles opciones de expansión, reduciendo así la búsqueda. En otras palabras, mientras que la tabla 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í el número de tablas resultantes que necesitan expandirse más.
Esto se puede ver en el siguiente ejemplo (proposicional). La tabla formada por una cadena para el conjunto de cláusulas se puede expandir en general utilizando cada una de las cuatro cláusulas de entrada, pero la conexión solo permite la expansión que utiliza . Esto significa que el árbol de tablas tiene cuatro hojas en general, pero solo una si se impone la conectividad. Esto significa que la conectividad deja solo una tabla para intentar expandir, en lugar de las cuatro que se deben considerar en general. A pesar de esta reducción de opciones, el teorema de completitud implica que se puede encontrar una tabla cerrada si el conjunto es insatisfacible.
Las condiciones de conectividad, cuando se aplican al caso proposicional (oclusivo), hacen que el cálculo resultante no sea confluente. Por ejemplo, es insatisfacible, pero al aplicarlo se genera la cadena , que no es cerrada y a la que no se puede aplicar ninguna otra regla de expansión sin violar ni la conectividad fuerte ni la débil. En el caso de la 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 insatisfacible del conjunto de cláusulas. Desafortunadamente, el problema de verificar si una cláusula cumple con esta condición es en sí mismo un problema difícil. A pesar de la no confluencia, se puede encontrar una tabla cerrada mediante la búsqueda, como se presenta en la sección "Búsqueda de una tabla cerrada" 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.
Una tabla es regular si ningún literal aparece dos veces en la misma rama. La aplicación de esta condición permite reducir las posibles opciones de expansión de la tabla, ya que las cláusulas que generarían una tabla no regular no se pueden expandir.
Sin embargo, estos pasos de expansión no permitidos 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 la tabla, es necesario expandir y cerrar, entre otras, la rama donde , donde aparece dos veces. Sin embargo, las fórmulas en esta rama son exactamente las mismas que las fórmulas de solo . Como resultado, los mismos pasos de expansión que cierran también 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, la expansión necesaria para cerrar estas hojas es completamente inútil; en el caso de primer orden, solo pueden afectar al resto de la tabla debido a algunas unificaciones; sin embargo, estas pueden combinarse con las sustituciones utilizadas para cerrar el resto de la tabla.
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 condiciones sobre un mundo posible, sino también sobre los 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, las tablas para lógicas modales se basan en la descomposición recursiva de fórmulas en sus componentes básicos. Sin embargo, la expansión de una fórmula modal puede requerir el establecimiento de condiciones para diferentes mundos. 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, la fórmula establece que es verdadera en el mundo actual y es falsa en un mundo al que se puede acceder desde él. Simplemente aplicando 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 cumplen en mundos diferentes. Los cálculos de cuadros modales contienen reglas del tipo de la anterior, pero incluyen mecanismos para evitar la interacción incorrecta de fórmulas que se refieren a mundos diferentes.
Técnicamente, las tablas para lógicas modales comprueban la satisfacibilidad de un conjunto de fórmulas: comprueban 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 que establece la verdad de en , la fórmula establece la verdad de en algún mundo al que se puede acceder desde y que, en general, puede ser diferente de . Los cálculos de tablas 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 cumplen en un mundo pueden implicar condiciones sobre diferentes sucesores de ese mundo. La insatisfacibilidad puede entonces probarse a partir del subconjunto de fórmulas que se refieren a un único sucesor. Esto se cumple si un mundo puede tener más de un sucesor, lo que 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 cumple y existe un sucesor donde se cumple. A la inversa, si uno puede demostrar la insatisfacibilidad de en un sucesor arbitrario, la fórmula se demuestra insatisfacible sin comprobar mundos donde se cumple. Al mismo tiempo, si uno puede demostrar la insatisfacibilidad de , no hay necesidad de comprobar . Como resultado, aunque hay dos formas posibles de expandir , una de estas dos formas siempre es suficiente para demostrar la insatisfacibilidad si la fórmula es insatisfacible. Por ejemplo, uno puede expandir la tabla considerando un mundo arbitrario donde se cumple. Si esta expansión conduce a la insatisfacibilidad, la fórmula original es insatisfacible. Sin embargo, también es posible que la insatisfacción no pueda probarse de esta manera, y que se debiera haber considerado en su lugar el mundo donde se cumple. Como resultado, siempre se puede probar la insatisfacción desarrollando solo o solo; sin embargo, si se hace la elección incorrecta, la tabla resultante puede no ser cerrada. Desarrollar cualquiera de las subfórmulas conduce a cálculos de tabla que son completos pero no confluentes en cuanto a la prueba. Por lo tanto, puede ser necesaria la búsqueda como se describe en "Búsqueda de una tabla cerrada".
Dependiendo de si la condición previa y la consecuencia de una regla de expansión de tabla 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 de tabla relativa (modal) 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 forma incorrecta es asegurarse de que todas las fórmulas de una rama hagan referencia al mismo mundo. Esta condición es inicialmente verdadera, ya que se supone que todas las fórmulas del conjunto cuya coherencia se va a comprobar hacen referencia al mismo mundo. Al expandir una rama, son posibles dos situaciones: o bien las nuevas fórmulas hacen referencia al mismo mundo que las otras de 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 cumplen también en el nuevo mundo se eliminan de la rama y, posiblemente, se añaden a todas las demás ramas que siguen siendo relativas al mundo antiguo.
Como ejemplo, en S5 cada fórmula que es verdadera en un mundo también es verdadera 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 estas también se cumplen en el nuevo mundo. Para mantener la integridad, las fórmulas eliminadas se agregan a todas las demás ramas que aún hacen referencia al mundo antiguo.
Un mecanismo diferente para asegurar la interacción correcta entre fórmulas que hacen referencia a mundos diferentes es cambiar de fórmulas a fórmulas etiquetadas: en lugar de escribir , uno escribiría para hacer explícito que se cumple en el mundo .
Todas las reglas de expansión proposicional se adaptan a esta variante al indicar que todas se refieren a fórmulas con la misma etiqueta de mundo. Por ejemplo, genera dos nodos etiquetados con y ; una rama se cierra solo si contiene dos literales opuestos del mismo mundo, como y ; no se genera ningún cierre si las dos etiquetas de mundo 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 la consecuencia de esta regla se refieren a los mundos y , respectivamente. Los diversos cálculos utilizan diferentes métodos para realizar un seguimiento de la accesibilidad de los mundos utilizados como etiquetas. Algunos incluyen pseudofórmulas como para indicar que es accesible desde . Otros utilizan secuencias de números enteros como etiquetas de mundo, 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 encuentran en mundos diferentes se puede solucionar utilizando tablas de etiquetado de conjuntos. Se trata de á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).
Las tablas para lógicas modales se utilizan para verificar la satisfacibilidad de un conjunto de fórmulas modales en una lógica modal dada. Dado un conjunto de fórmulas , verifican 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 tablas para la lógica modal básica K añadiendo a las reglas de tablas proposicionales 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 en algunos mundos accesibles. La consecuencia de esta regla es una fórmula que debe ser verdadera en uno de esos mundos donde es verdadera.
En términos más técnicos, los métodos de tablas modales comprueban la existencia de un modelo y un mundo que hacen que un conjunto de fórmulas sea verdadero. Si son verdaderas en , debe haber un mundo al que se pueda acceder desde y que haga que sean verdaderas. Por lo tanto, esta regla equivale a derivar un conjunto de fórmulas que deben cumplirse en tales .
Si bien se supone que las condiciones previas se cumplen en , se supone que las consecuencias se cumplen en : mismo modelo pero posiblemente mundos diferentes. Las tablas etiquetadas por conjuntos no registran explícitamente el mundo en el que se supone que cada fórmula es verdadera: dos nodos pueden o no referirse al mismo mundo. Sin embargo, las fórmulas que etiquetan cualquier nodo dado se suponen verdaderas en el mismo mundo.
Como resultado de la posibilidad de que existan diferentes mundos en los que se supone que las fórmulas son 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 tablas de etiquetado de conjuntos, ya que las reglas de expansión se basan solo en la hoja en la que se aplican y no en sus antecesores.
En particular, no se extiende directamente a múltiples fórmulas negadas en caja como en : si bien existe un mundo accesible donde es falso y uno en el que es falso, estos dos mundos no son necesariamente iguales.
A diferencia de las reglas proposicionales, los estados condicionan todas sus precondiciones. Por ejemplo, no se puede aplicar a un nodo etiquetado por ; si bien este conjunto es inconsistente y esto podría demostrarse 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: una tabla para un conjunto inconsistente puede ser imposible de cerrar, incluso si existe una tabla cerrada para el mismo conjunto.
La regla no es determinista: el conjunto de fórmulas que se deben eliminar (o conservar) se puede elegir de manera arbitraria; esto crea el problema de elegir un conjunto de fórmulas para descartar que no sea tan grande como para que el conjunto resultante sea satisfacible ni tan pequeño como para que las reglas de expansión necesarias sean inaplicables. Tener una gran cantidad de opciones posibles dificulta el problema de buscar una tabla cerrada.
Este no determinismo se puede evitar restringiendo el uso de de modo que solo se aplique antes de una regla de expansión modal y de modo que solo elimine las fórmulas que hacen que esa otra regla sea inaplicable. Esta condición también se puede formular fusionando las dos reglas en una sola. La regla resultante produce el mismo resultado que la anterior, pero descarta implícitamente todas las fórmulas que hicieron que la regla anterior fuera inaplicable. Se ha demostrado que este mecanismo de eliminación preserva la completitud 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 de la tabla correspondiente es:
Esta regla relaciona condiciones sobre el mismo mundo: si es verdadera en un mundo, por reflexividad también es verdadera en el mismo mundo . Esta regla es estática, no transaccional, ya que tanto su precondición como su consecuente se refieren al mismo mundo.
Esta regla copia de la condición previa a la consecuente, a pesar de que esta fórmula se haya "utilizado" para generar . Esto es correcto, ya que el mundo considerado es el mismo, por lo que también se cumple allí. Esta "copia" es necesaria en algunos casos. Por ejemplo, es necesario demostrar la inconsistencia de : las únicas reglas aplicables son en orden , del cual se bloquea uno 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 nuevo mundo que se introduce en el cuadro. Por ejemplo, implica que es falso en un mundo accesible, por lo que se comienza un nuevo cuadro con raíz en . Este nuevo cuadro se adjunta al nodo del cuadro original donde se ha aplicado la regla de expansión; un cierre de este cuadro genera inmediatamente un cierre de todas las ramas donde está 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.
Las tablas modales anteriores establecen la consistencia de un conjunto de fórmulas y pueden utilizarse para resolver el problema de la consecuencia lógica local . Se trata del problema de determinar si, para cada modelo , si es cierto en un mundo , entonces también es cierto en el mismo mundo. Esto es lo mismo que comprobar si es cierto en un mundo de un modelo, en el supuesto de que también es cierto en el mismo mundo del mismo modelo.
Un problema relacionado es el problema de la consecuencia global, en el que 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, donde es verdadera en todos los mundos, también es verdadera en todos los mundos.
Los supuestos locales y globales difieren en los modelos en los que la fórmula asumida es verdadera en algunos mundos pero no en otros. Por ejemplo, la implicación es global pero no local. La implicación local no se cumple en un modelo que consta de dos mundos que hacen que y sean verdaderos, respectivamente, y donde el segundo es accesible desde el primero; en el primer mundo, los supuestos son verdaderos pero son falsos. Este contraejemplo funciona porque se puede suponer que son verdaderos en un mundo y falsos en otro. Sin embargo, si el mismo supuesto se considera global, no se permite en ningún mundo del modelo.
Estos dos problemas se pueden combinar, de modo que se pueda verificar si es una consecuencia local de bajo el supuesto global . Los cálculos de tablas pueden tratar el supuesto global mediante una regla que permita 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 tablas, las fórmulas suelen denotarse mediante una convención, de modo que, por ejemplo, siempre se considera que es . La siguiente tabla proporciona la notación para fórmulas en lógica proposicional, de primer orden y modal.
Cada etiqueta de la primera columna se considera una fórmula de las otras columnas. Una fórmula con líneas superpuestas como indica que es la negación de cualquier fórmula que aparezca en su lugar, de modo que, por ejemplo, en fórmula la subfórmula es la negación de .
Como 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 desarrollo de la conjunción se formula como:
Se supone que una fórmula en una tabla es verdadera. Las tablas con signo permiten indicar que una fórmula es falsa. Esto se logra generalmente 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 escribir las fórmulas que se suponen verdaderas a la izquierda del nodo y las fórmulas que se suponen falsas a su derecha.
