Método de cuadros analíticos

Supongamos un conjunto infinito${\displaystyle PV}$de variables proposicionales y definir el conjunto${\displaystyle \Phi }$de fórmulas por inducción, representadas por la siguiente gramática:

${\displaystyle \Phi$ ::=PV\mid \neg \Phi \mid (\Phi \to \Phi )\mid (\Phi \lor \Phi )\mid (\Phi \land \Phi )} .

Es decir, los conectores básicos son: negación${\displaystyle \neg }$, implicación${\displaystyle \to }$, disyunción${\displaystyle \lor }$y conjunción${\displaystyle \land }$.

La veracidad o falsedad de una fórmula 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 variables proposicionales tal que la fórmula completa, que combina las variables con conectores, sea también verdadera. ^{[ 1 ]} Se dice que dicha asignación satisface la fórmula. ^{[ 2 ]}

Un tableau comprueba si un conjunto dado de fórmulas es satisfacible o no. Puede utilizarse para comprobar la validez o la implicación: una fórmula es válida si su negación es insatisfacible, y las fórmulas${\displaystyle A_{1},\ldots ,A_{n}}$implicar${\displaystyle B}$si${\displaystyle \{A_{1},\ldots ,A_{n},\neg B\}}$es insatisfactorio.

Para cualquier fórmula${\displaystyle X}$,${\displaystyle Y}$Se cumplen los siguientes hechos:

• Si una conjunción${\displaystyle X\land Y}$    Si es cierto, entonces${\displaystyle X}$,${\displaystyle Y}$ambas son verdaderas; es falsa, entonces o    ${\displaystyle X}$es falso o${\displaystyle Y}$es falso.
• Si una disyunción${\displaystyle X\lor Y}$    es cierto, entonces o${\displaystyle X}$es cierto o${\displaystyle Y}$es verdadero; es falso, entonces    ${\displaystyle X}$,${\displaystyle Y}$ambas son falsas.
• Si una condición${\displaystyle X\to Y}$    es cierto, entonces o${\displaystyle X}$es falso o${\displaystyle Y}$es verdadero; es falso, entonces    ${\displaystyle X}$es cierto y${\displaystyle Y}$es falso.
• Si una negación${\displaystyle \neg X}$    Si es cierto, entonces${\displaystyle X}$es falso; es falso, entonces    ${\displaystyle X}$Es cierto.

El método de los tableaux analíticos se basa en estos hechos. El principio fundamental de los tableaux proposicionales consiste en intentar "descomponer" fórmulas complejas en fórmulas más pequeñas hasta obtener pares de literales complementarios o hasta que no sea posible una mayor expansión.

El método opera 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 a probar insatisfacibilidad. ^{[ 11 ]} Luego, el siguiente procedimiento puede aplicarse repetidamente de forma no determinista:

1. Seleccione un nodo hoja abierto. (El nodo hoja en la cadena inicial está marcado como abierto).
2. Seleccione un nodo aplicable en la rama superior al nodo seleccionado. ^{[ 12 ]}
3. Aplique el nodo correspondiente, que consiste en expandir el árbol debajo del nodo hoja seleccionado según alguna regla de expansión (que se detalla a continuación).
4. Para cada nodo recién creado que sea a la vez un literal/literal negado, y cuyo complemento aparezca en un nodo anterior en la misma rama, marque la rama como cerrada . Marque todos los demás nodos recién creados como abiertos .

Si una rama del cuadro contiene una fórmula...

• ${\displaystyle {\boldsymbol {\mathsf {T}}}(X\land Y)}$, añade a su hoja la cadena de dos nodos que contienen las fórmulas${\displaystyle {\boldsymbol {\mathsf {T}}}(X)}$y${\displaystyle {\boldsymbol {\mathsf {T}}}(Y)}$; ^{[ 13 ]}
• ${\displaystyle {\boldsymbol {\mathsf {F}}}(X\land Y)}$, crea dos hijos hermanos a su hoja, que contienen las fórmulas${\displaystyle {\boldsymbol {\mathsf {F}}}(X)}$y${\displaystyle {\boldsymbol {\mathsf {F}}}(Y)}$respectivamente; ^{[ 14 ]}
• ${\displaystyle {\boldsymbol {\mathsf {T}}}(X\lor Y)}$, crea dos hijos hermanos a su hoja, que contienen las fórmulas${\displaystyle {\boldsymbol {\mathsf {T}}}(X)}$y${\displaystyle {\boldsymbol {\mathsf {T}}}(Y)}$respectivamente;
• ${\displaystyle {\boldsymbol {\mathsf {F}}}(X\lor Y)}$, añade a su hoja la cadena de dos nodos que contienen las fórmulas${\displaystyle {\boldsymbol {\mathsf {F}}}(X)}$y${\displaystyle {\boldsymbol {\mathsf {F}}}(Y)}$;
• ${\displaystyle {\boldsymbol {\mathsf {T}}}(X\to Y)}$, crea dos hijos hermanos a su hoja, que contienen las fórmulas${\displaystyle {\boldsymbol {\mathsf {F}}}(X)}$y${\displaystyle {\boldsymbol {\mathsf {T}}}(Y)}$respectivamente;
• ${\displaystyle {\boldsymbol {\mathsf {F}}}(X\to Y)}$, añade a su hoja la cadena de dos nodos que contienen las fórmulas${\displaystyle {\boldsymbol {\mathsf {T}}}(X)}$y${\displaystyle {\boldsymbol {\mathsf {F}}}(Y)}$;
• ${\displaystyle {\boldsymbol {\mathsf {T}}}(\neg X)}$, añade a su hoja el nodo que contiene la fórmula${\displaystyle {\boldsymbol {\mathsf {F}}}(X)}$;
• ${\displaystyle {\boldsymbol {\mathsf {F}}}(\neg X)}$, añade a su hoja el nodo que contiene la fórmula${\displaystyle {\boldsymbol {\mathsf {T}}}(X)}$.

El proceso de descomposición finaliza después de un número finito de pasos, porque cada aplicación de una regla elimina un conector, y solo hay un número finito de conectores en cualquier fórmula.

Nota : En sistemas basados ​​en la gramática

${\displaystyle \Phi$ ::=\bot \mid PV\mid (\Phi \to \Phi )\mid (\Phi \lor \Phi )\mid (\Phi \land \Phi )} ,

que no tratan la negación como algo primitivo, sino que la definen en términos de implicación y falsedad (${\displaystyle \neg \Phi \,{\overset {\text{def}}{=}}\,\Phi \to \bot }$), las reglas del tablero para${\displaystyle \neg }$son reemplazados por

El principio de la tabla consiste en considerar las fórmulas en nodos de la misma rama como conjunciones, mientras que las ramas diferentes se consideran disyuntas. Como resultado, una tabla es una representación arbórea de una fórmula que es una disyunción de conjunciones. Esta fórmula es equivalente al conjunto para probar 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 dicha conjunción es insatisfacible. Si se demuestra que todas las conjunciones son insatisfacibles, el conjunto original de fórmulas es insatisfacible.

Cada tableau puede considerarse como una representación gráfica de una fórmula, equivalente al conjunto a partir del cual se construye. Esta fórmula es la siguiente: cada rama del tableau representa la conjunción de sus fórmulas; el tableau representa la disyunción de sus ramas. Las reglas de expansión transforman un tableau en uno que tiene una fórmula representada equivalente. Dado que el tableau se inicializa como una sola rama que contiene las fórmulas del conjunto de entrada, todos los tableaux subsiguientes obtenidos a partir de él representan fórmulas equivalentes a ese conjunto (en la variante donde el tableau inicial es el único nodo etiquetado como verdadero, las fórmulas representadas por los tableaux son consecuencias del conjunto original).

El método de los tableaux funciona partiendo de un conjunto inicial de fórmulas y añadiendo fórmulas cada vez más simples hasta que se muestra una contradicción en forma simple de literales opuestos. Dado que la fórmula representada por un tableau es la disyunción de las fórmulas representadas por sus ramas, se obtiene una contradicción 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 puede ahora "cerrarse", ya que no es necesario expandirla más. Si todas las ramas de un tableau están cerradas, la fórmula representada por el tableau es insatisfacible; por lo tanto, el conjunto original también lo es. Obtener un tableau 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 demuestra por la imposibilidad de encontrar un tableau cerrado, siempre que se haya aplicado cada regla de expansión en todos los lugares donde se podría aplicar. En particular, si un tableau 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 considera que una fórmula puede aparecer en más de una rama (esto ocurre si existe al menos un punto de ramificación "debajo" del nodo). En este caso, se debe aplicar la regla para expandir la fórmula de manera que su(s) conclusión(es) se añadan a todas las ramas que aún estén abiertas, antes de poder concluir que el tableau no se puede expandir más y que, por lo tanto, la fórmula es satisfacible.

Las reglas anteriores para el tableau proposicional se pueden simplificar utilizando la notación uniforme. En la notación uniforme, cada fórmula es de tipo${\displaystyle \alpha }$(alfa) o de tipo${\displaystyle \beta }$(beta). A cada fórmula de tipo alfa se le asignan los dos componentes.${\displaystyle \alpha _{1},\alpha _{2}}$y a cada fórmula de tipo beta se le asignan los dos componentes.${\displaystyle \beta _ {1}, \beta _ {2}}$Las fórmulas de tipo alfa pueden considerarse conjuntivas, ya que ambas${\displaystyle \alpha _{1}}$y${\displaystyle \alpha _{2}}$están implícitos por${\displaystyle \alpha }$siendo cierto. Las fórmulas de tipo beta pueden considerarse disyuntivas, ya que o bien${\displaystyle \beta _{1}}$o${\displaystyle \beta _{2}}$está implícito por${\displaystyle \beta }$siendo cierto. Las tablas a continuación muestran cómo determinar el tipo y los componentes de cualquier fórmula proposicional dada . ^{[ 15 ]}

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 componentes respectivos.

Al construir un cuadro proposicional utilizando la notación anterior, siempre que se encuentre una fórmula de tipo alfa, sus dos componentes${\displaystyle \alpha _{1},\alpha _{2}}$se agregan a la rama actual que se está expandiendo. Siempre que uno encuentra una fórmula de tipo beta en alguna rama${\displaystyle \theta }$uno puede dividir${\displaystyle \theta }$en dos ramas, una con el conjunto {${\displaystyle \theta }$,${\displaystyle \beta _{1}}$} de fórmulas, y el otro con el conjunto {${\displaystyle \theta }$,${\displaystyle \beta _{2}}$} de fórmulas. ^{[ 16 ]}

Una variante del tableau consiste en etiquetar los nodos con conjuntos de fórmulas en lugar de fórmulas individuales. ^{[ 17 ]} En este caso, el tableau inicial es un nodo único etiquetado con el conjunto que se debe demostrar que es satisfacible. Por lo tanto, las fórmulas de un conjunto se consideran en conjunción.

Las reglas de expansión del tablero ahora pueden funcionar en las hojas del tablero, ignorando todos los nodos internos. Para la conjunción, la regla se basa en la equivalencia de un conjunto que contiene una conjunción.${\displaystyle A\land B}$con el conjunto que contiene ambos${\displaystyle A}$y${\displaystyle B}$en su lugar. En particular, si una hoja está etiquetada con${\displaystyle X\cup \{A\land B\}}$, se le puede agregar un nodo con etiqueta${\displaystyle X\cup \{A,B\}}$:

${\displaystyle (\land ){\frac {X\cup \{A\land B\}}{X\cup \{A,B\}}}}$

Para la disyunción, un conjunto${\displaystyle X\cup \{A\lor B\}}$es equivalente a la disyunción de los dos conjuntos${\displaystyle X\cup \{A\}}$y${\displaystyle X\cup \{B\}}$. Como resultado, si el primer conjunto etiqueta una hoja, se le pueden agregar dos hijos, etiquetados con las dos últimas fórmulas.

${\displaystyle (\lor ){\frac {X\cup \{A\lor B\}}{X\cup \{A\}|X\cup \{B\}}}}$

Finalmente, si un conjunto contiene tanto un literal como su negación, esta rama puede cerrarse:

${\displaystyle (id){\frac {X\cup \{p,\neg p\}}{closed}}}$

Un tableau para un conjunto finito X dado es un árbol finito (invertido) con raíz X, en el que todos los nodos hijos se obtienen aplicando las reglas del tableau a sus padres. Una rama en dicho tableau está cerrada si su nodo hoja contiene "cerrado". Un tableau está cerrado si todas sus ramas están cerradas. Un tableau está abierto si al menos una rama no está cerrada.

A continuación se muestran dos cuadros cerrados para el conjunto.

${\displaystyle X=\{r\land \neg r,\;p\land ((\neg p\lor q)\land \neg q)\}}$

Cada aplicación de regla está marcada en el lado derecho. Ambas logran el mismo efecto; la primera cierra más rápido. La única diferencia radica en el orden en que se realiza la reducción.

${\displaystyle {\dfrac {\quad {\dfrac {\quad r\land \neg r,\;p\land ((\neg p\lor q)\land \neg q)\quad }{r,\;\neg r,\;p\land ((\neg p\lor q)\land \neg q)}}(\land )}{closed}}(\land )}$

y una segunda, más larga, con las reglas aplicadas en un orden diferente:

${\displaystyle {\dfrac {\quad {\dfrac {\quad {\dfrac {\quad r\land \neg r,\;p\land ((\neg p\lor q)\land \neg q)\quad }{r\land \neg r,\;p,\;((\neg p\lor q)\land \neg q)}}(\land )\quad }{r\land \neg r,\;p,\;(\neg p\lor q),\;\neg q}}(\land )}{\quad {\dfrac {\quad r\land \neg r,\;p,\;\neg p,\;\neg q\quad }{closed}}(id)\quad \quad {\dfrac {\quad r\land \neg r,\;p,\;q,\;\neg q\quad }{closed}}(id)}}(\lor )}$

El primer tableau se cierra tras la aplicación de una sola regla, mientras que el segundo no lo consigue y tarda mucho más en cerrarse. Evidentemente, lo ideal sería encontrar siempre el tableau cerrado más corto, pero se puede demostrar que no existe un único algoritmo que lo encuentre para todos los conjuntos de fórmulas de entrada.

Las tres reglas${\displaystyle (\land )}$,${\displaystyle (\lor )}$y${\displaystyle (id)}$lo anterior es suficiente para decidir si un conjunto dado${\displaystyle X'}$de fórmulas en forma normal negada son conjuntamente satisfacibles:

Simplemente aplica todas las reglas posibles en todos los órdenes posibles hasta que encontremos un tablero cerrado para${\displaystyle X'}$o hasta que agotemos todas las posibilidades y concluyamos que cada cuadro para${\displaystyle X'}$está abierto.

En el primer caso,${\displaystyle X'}$es conjuntamente insatisfacible y en el segundo caso el nodo hoja de la rama abierta da una asignación a las fórmulas atómicas y fórmulas atómicas negadas que hacen${\displaystyle X'}$conjuntamente satisfacible. La lógica clásica tiene en realidad la propiedad bastante agradable de que solo necesitamos investigar (cualquiera) un tableau completamente: si se cierra entonces${\displaystyle X'}$es insatisfactorio y si está abierto entonces${\displaystyle X'}$es satisfacible. Pero esta propiedad no la poseen generalmente otras lógicas.

Estas reglas son suficientes para toda la lógica clásica, ya que, partiendo de un conjunto inicial de fórmulas X , reemplazamos cada elemento C por su forma normal negada lógicamente equivalente C', obteniendo así un conjunto de fórmulas X' . Sabemos que X es satisfacible si y solo si X' es satisfacible, por lo que basta con buscar un tableau cerrado para X' siguiendo el procedimiento descrito anteriormente.

Al establecer${\displaystyle X=\{\neg A\}}$Se puede comprobar si la fórmula A es una tautología de la lógica clásica:

Si el cuadro para${\displaystyle \{\neg A\}}$cierra entonces${\displaystyle \neg A}$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${\displaystyle \{\neg A\}}$da una tarea que falsifica A.

Una fórmula de primer orden${\displaystyle \forall x.\gamma (x)}$implica todas las fórmulas${\displaystyle \gamma (t)}$dónde${\displaystyle t}$es un término fundamental . Por lo tanto, la siguiente regla de inferencia es correcta:

${\displaystyle (\forall ){\frac {\forall x.\gamma (x)}{\gamma (t)}}}$dónde${\displaystyle t}$es un término base arbitrario

A diferencia de las reglas para los conectores proposicionales, pueden ser necesarias múltiples aplicaciones de esta regla a la misma fórmula. Como ejemplo, el conjunto${\displaystyle \{\neg P(a)\lor \neg P(b),\forall x.P(x)\}}$solo se puede demostrar que es insatisfactorio si ambos${\displaystyle P(a)}$y${\displaystyle P(b)}$se generan a partir de${\displaystyle \forall x.P(x)}$.

Los cuantificadores existenciales se tratan mediante la skolemización. En particular, una fórmula con un cuantificador existencial principal como${\displaystyle \exists x.\delta (x)}$genera su skolemización${\displaystyle \delta (c)}$, dónde${\displaystyle c}$es un nuevo símbolo constante.

${\displaystyle (\exists ){\frac {\exists x.\delta (x)}{\delta (c)}}}$dónde${\displaystyle c}$es un nuevo símbolo constante

El término Skolem${\displaystyle c}$es una constante (una función de aridad 0) porque la cuantificación sobre${\displaystyle x}$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${\displaystyle x}$Estaba dentro de su ámbito, estos cuantificadores evidentemente han sido eliminados por la aplicación de la regla para cuantificadores universales.

La regla para cuantificadores existenciales introduce nuevos símbolos constantes. Estos símbolos pueden ser utilizados por la regla para cuantificadores universales, de modo que${\displaystyle \forall y.\gamma (y)}$puede generar${\displaystyle \gamma (c)}$incluso si${\displaystyle c}$no estaba en la fórmula original, sino que es una constante de Skolem creada por la regla para cuantificadores existenciales.

Las dos reglas anteriores para cuantificadores universales y existenciales son correctas, al igual que las reglas proposicionales: si un conjunto de fórmulas genera un tableau cerrado, este conjunto es insatisfacible. También se puede demostrar la completitud: si un conjunto de fórmulas es insatisfacible, existe un tableau cerrado construido a partir de él mediante estas reglas. Sin embargo, encontrar realmente dicho tableau cerrado requiere una política adecuada de aplicación de las reglas. De lo contrario, un conjunto insatisfacible puede generar un tableau de crecimiento infinito. Como ejemplo, el conjunto${\displaystyle \{\neg P(f(c)),\forall x.P(x)\}}$es insatisfacible, pero nunca se obtiene un cuadro cerrado si uno imprudentemente sigue aplicando la regla para cuantificadores universales a${\displaystyle \forall x.P(x)}$generando, por ejemplo,${\displaystyle P(c),P(f(c)),P(f(f(c))),\ldots }$Siempre se puede encontrar un tableau cerrado descartando esta y otras políticas "injustas" similares de aplicación de las reglas del tableau.

La regla para cuantificadores universales${\displaystyle (\forall )}$Es la única regla no determinista, ya que no especifica con qué término instanciar. Además, mientras que las demás reglas solo necesitan aplicarse una vez por 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 puede restringirse retrasando su aplicación hasta que ninguna otra regla sea aplicable y restringiéndola a los términos base que ya aparecen en la ruta del tableau. La variante de tableaux con unificación que se muestra a continuación busca resolver el problema del no determinismo.

El principal problema de un cuadro sin unificación es cómo elegir un término base.${\displaystyle t}$para la regla del cuantificador universal. De hecho, se puede usar cualquier término base posible, 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 tableau. Esto se puede hacer utilizando una variable en lugar de un término, de modo que${\displaystyle \forall x.\gamma (x)}$genera${\displaystyle \gamma (x')}$y luego permitir sustituciones para reemplazar posteriormente${\displaystyle x'}$con un término. La regla para cuantificadores universales se convierte en:

${\displaystyle (\forall ){\frac {\forall x.\gamma (x)}{\gamma (x')}}}$dónde${\displaystyle x'}$es una variable que no aparece en ningún otro lugar de la tabla

Si bien se supone que el conjunto inicial de fórmulas no contiene variables libres, una fórmula del tableau 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 base. La ventaja de este cambio es que estas variables pueden recibir un valor cuando se cierra una rama del tableau, lo que resuelve el problema de generar términos que podrían resultar inútiles.

Por ejemplo,${\displaystyle \{\neg P(a),\forall x.P(x)\}}$se puede demostrar que es insatisfacible generando primero${\displaystyle P(x_{1})}$; la negación de este literal es unificable con${\displaystyle \neg P(a)}$, siendo el unificador más general la sustitución que reemplaza${\displaystyle x_{1}}$con${\displaystyle a}$; al aplicar esta sustitución se obtiene reemplazar${\displaystyle P(x_{1})}$con${\displaystyle P(a)}$, lo que cierra el cuadro.

Esta regla cierra al menos una rama del tableau: la que contiene el par de literales considerado. Sin embargo, la sustitución debe aplicarse a todo el tableau, no solo a estos dos literales. Esto se expresa diciendo que las variables libres del tableau 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 (implícitamente) universalmente y todas las fórmulas del tableau están dentro del alcance de estos cuantificadores.

Los cuantificadores existenciales se tratan mediante la skolemización. A diferencia del tableau sin unificación, los términos de skolem pueden no ser constantes simples. De hecho, las fórmulas en un tableau con unificación pueden contener variables libres, que se consideran implícitamente cuantificadas universalmente. Como resultado, una fórmula como${\displaystyle \exists x.\delta (x)}$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.

${\displaystyle (\exists ){\frac {\exists x.\delta (x)}{\delta (f(x_{1},\ldots ,x_{n}))}}}$dónde${\displaystyle f}$es un nuevo símbolo de función y${\displaystyle x_{1},\ldots ,x_{n}}$las variables libres de${\displaystyle \delta }$

Esta regla incorpora una simplificación sobre una regla donde${\displaystyle x_{1},\ldots ,x_{n}}$son las variables libres de la rama, no de${\displaystyle \delta }$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${\displaystyle \delta }$hasta el cambio de nombre de las variables.

La fórmula representada por un tableau se obtiene de forma similar al caso proposicional, con la suposición adicional de que las variables libres se consideran cuantificadas universalmente. Al igual que en el caso proposicional, las fórmulas de cada rama se combinan y las fórmulas resultantes se separan. Además, todas las variables libres de la fórmula resultante están cuantificadas universalmente. Todos estos cuantificadores abarcan toda la fórmula. En otras palabras, si${\displaystyle F}$es la fórmula obtenida al separar la conjunción de las fórmulas en cada rama, y${\displaystyle x_{1},\ldots ,x_{n}}$son las variables libres en él, entonces${\displaystyle \forall x_{1},\ldots ,x_{n}.F}$es la fórmula representada por la tabla. Se aplican las siguientes consideraciones:

• La suposición de que las variables libres están cuantificadas universalmente es lo que hace que la aplicación de un unificador más general sea una regla sólida: dado que${\displaystyle \gamma (x')}$significa que${\displaystyle \gamma }$es cierto para cada valor posible de${\displaystyle x'}$, entonces${\displaystyle \gamma (t)}$es cierto para el término${\displaystyle t}$que el unificador más general reemplaza${\displaystyle x}$con.
• Las variables libres en un tableau son rígidas: todas las ocurrencias de la misma variable deben ser reemplazadas por el mismo término. Cada variable puede considerarse un símbolo que representa un término que aún no se ha decidido. Esto es consecuencia de asumir que las variables libres están cuantificadas universalmente sobre toda la fórmula representada por el tableau: si la misma variable aparece libre en dos nodos diferentes, ambas ocurrencias están dentro del alcance del mismo cuantificador. Por ejemplo, si las fórmulas en dos nodos son${\displaystyle A(x)}$y${\displaystyle B(x)}$, dónde${\displaystyle x}$es libre en ambos, la fórmula representada por el cuadro es algo en la forma${\displaystyle \forall x.(...A(x)...B(x)...)}$Esta fórmula implica que${\displaystyle (...A(x)...B(x)...)}$es cierto para cualquier valor de${\displaystyle x}$pero en general no implica${\displaystyle (...A(t)...A(t')...)}$para dos términos diferentes${\displaystyle t}$y${\displaystyle t'}$, ya que estos dos términos pueden, en general, tomar valores diferentes. Esto significa que${\displaystyle x}$no puede ser reemplazado por dos términos diferentes en${\displaystyle A(x)}$y${\displaystyle B(x)}$.
• Las variables libres en una fórmula para verificar su validez también se consideran cuantificadas universalmente. Sin embargo, estas variables no pueden dejarse libres al construir un tableau, porque las reglas del tableau funcionan de forma inversa a la fórmula, pero siguen tratando las variables libres como cuantificadas universalmente. Por ejemplo,${\displaystyle P(x)\to P(c)}$no es válido (no es cierto en el modelo donde${\displaystyle D=\{1,2\},P(1)=\bot ,P(2)=\top ,c=1}$y la interpretación donde${\displaystyle x=2}$). Como consecuencia,${\displaystyle \{P(x),\neg P(c)\}}$es satisfacible (es satisfecha por el mismo modelo e interpretación). Sin embargo, se podría generar un tableau cerrado con${\displaystyle P(x)}$y${\displaystyle \neg P(c)}$y sustituyendo${\displaystyle x}$con${\displaystyle c}$generaría un cierre. Un procedimiento correcto es primero hacer explícitos los cuantificadores universales, generando así${\displaystyle \forall x.(P(x)\to P(c))}$.

Las dos variantes siguientes también son correctas.

• Aplicar una sustitución a las variables libres de la tabla completa es una regla correcta, siempre que dicha sustitución sea válida para la fórmula que representa la tabla. En otras palabras, aplicar tal sustitución da como resultado una tabla cuya fórmula sigue siendo consecuencia del conjunto de entrada. El uso de la mayoría de los unificadores generales garantiza automáticamente que se cumpla la condición de libertad para la tabla.
• Si bien, en general, todas las variables deben reemplazarse por el mismo término en toda la tabla, existen algunos casos especiales en los que esto no es necesario.

Se puede demostrar que los tableaux con unificación son completos: si un conjunto de fórmulas es insatisfacible, existe una prueba de tableaux con unificación. Sin embargo, encontrar dicha prueba puede ser un problema complejo. A diferencia del caso sin unificación, aplicar una sustitución puede modificar la parte existente de un tableaux; si bien una sustitución cierra al menos una rama, puede hacer que otras ramas sean imposibles de cerrar (incluso si el conjunto es insatisfacible).

Una solución a este problema es la instanciación diferida : no se aplica ninguna sustitución hasta que se encuentre una que cierre todas las ramas simultáneamente. Con esta variante, siempre se puede encontrar una prueba de que un conjunto es insatisfacible mediante una política adecuada de aplicación de las demás reglas. Sin embargo, este método requiere que todo el tableau 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 algunos tableaux generados sean imposibles de cerrar, incluso si el conjunto es insatisfacible, es común a otros conjuntos de reglas de expansión de tableaux: aunque ciertas secuencias de aplicación de estas reglas permiten construir un tableaux cerrado (si el conjunto es insatisfacible), otras secuencias dan lugar a tableaux que no se pueden cerrar. Las soluciones generales para estos casos se describen en la sección "Búsqueda de un tableaux".

El tamaño del árbol de búsqueda depende del número de tablas (hijas) que se pueden generar a partir de una tabla (padre) dada. Por lo tanto, reducir el número de dichas tablas reduce el tiempo de búsqueda necesario.

Una forma de reducir este número es impedir la generación de ciertos tableaux en función de 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, ya que la rama que contiene dos copias del literal tendría el mismo conjunto de fórmulas que la original. Esta expansión puede impedirse porque, si existe un tableau cerrado, se puede encontrar sin ella. Esta restricción es estructural, ya que se puede verificar examinando la estructura del tableau que se va a expandir.

Diferentes métodos para reducir la búsqueda impiden la generación de algunos tableaux basándose en que aún se puede encontrar un tableau cerrado expandiendo los demás. 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 debe expandirse. En consecuencia, si un tableau tiene, por ejemplo, dos ramas no cerradas, la regla especifica cuál debe expandirse, impidiendo la expansión de la segunda. Esta restricción reduce el espacio de búsqueda porque ahora se prohíbe una posible elección; sin embargo, la completitud no se ve afectada, ya que la segunda rama se seguirá expandiendo si la primera se cierra finalmente. Como ejemplo, un tableau con raíz${\displaystyle \neg a\land \neg b}$, niño${\displaystyle a\lor b}$y dos hojas${\displaystyle a}$y${\displaystyle b}$se puede cerrar de dos maneras: aplicando${\displaystyle (\land )}$primero a${\displaystyle a}$y luego a${\displaystyle b}$o viceversa. Claramente no hay necesidad de seguir ambas posibilidades; uno puede considerar solo el caso en el que${\displaystyle (\land )}$se aplica primero a${\displaystyle a}$y desestimar el caso en el que se aplica por primera vez a${\displaystyle b}$. Esta es una restricción global porque lo que permite descuidar esta segunda expansión es la presencia del otro tablero, donde se aplica la expansión a${\displaystyle a}$primero y${\displaystyle b}$después.

Connection es una condición sobre tableau que prohíbe expandir una rama usando cláusulas que no estén relacionadas con los literales que ya están en la rama. Connection se puede definir de dos maneras:

fuerte conexión

Al expandir una rama, utilice una cláusula de entrada solo si contiene un literal que pueda unificarse con la negación del literal en la hoja actual.

conectividad débil

permitir el uso de cláusulas que contienen un literal que se unifica con la negación de un literal en la rama

Ambas condiciones se aplican únicamente a ramas que no constan solo 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 restringe aún más que ese literal se encuentre en una hoja de la rama actual.

Si la expansión de la cláusula está restringida por la conexión (fuerte o débil), su aplicación produce un cuadro en el que la sustitución se puede aplicar 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 la hoja padre, en caso de conexión fuerte).

Ambas condiciones de conectividad conducen a un cálculo completo de primer orden: si un conjunto de cláusulas es insatisfacible, posee un tableau cerrado conectado (fuerte o débilmente). Dicho tableau cerrado puede hallarse mediante una búsqueda en el espacio de tableaux, como se explica en la sección «Búsqueda de un tableau cerrado». Durante esta búsqueda, la conectividad elimina algunas opciones de expansión posibles, reduciendo así la búsqueda. En otras palabras, si bien el tableau en un nodo del árbol puede expandirse de varias maneras diferentes, la conectividad solo permite unas pocas, reduciendo así el número de tableaux resultantes que necesitan expandirse posteriormente.

Esto se puede ver en el siguiente ejemplo (proposicional). El cuadro formado por una cadena${\displaystyle true-a}$para el conjunto de cláusulas${\displaystyle \{a,\neg a\lor b,\neg c\lor d,\neg b\}}$en general se puede expandir utilizando cada una de las cuatro cláusulas de entrada, pero la conexión solo permite la expansión que utiliza${\displaystyle \neg a\lor b}$Esto significa que el árbol de tableaux tiene cuatro hojas en general, pero solo una si se impone la conexidad. Esto implica que la conexidad deja solo un tableau para intentar expandir, en lugar de los cuatro que se suelen considerar. A pesar de esta reducción de opciones, el teorema de completitud implica que se puede encontrar un tableau cerrado si el conjunto es insatisfacible.

Las condiciones de conectividad, cuando se aplican al caso proposicional (clausal), hacen que el cálculo resultante no sea confluente. Como ejemplo,${\displaystyle \{a,b,\neg b\}}$es insatisfactorio, pero aplicar${\displaystyle (C)}$a${\displaystyle a}$genera la cadena${\displaystyle true-a}$, que no está cerrado y al que no se le puede aplicar ninguna otra regla de expansión sin violar la conectividad 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 insatisfacible 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 falta de confluencia, se puede encontrar un tableau cerrado mediante la búsqueda, como se presenta en la sección anterior "Búsqueda de un tableau cerrado". Si bien la búsqueda es necesaria, la conectividad reduce las posibles opciones de expansión, lo que hace que la búsqueda sea más eficiente.

Un tableau es regular si ningún literal aparece dos veces en la misma rama. Al imponer esta condición, se reduce el número de opciones posibles para la expansión del tableau, ya que las cláusulas que generarían un tableau no regular no se pueden expandir.

Sin embargo, estos pasos de expansión no permitidos son inútiles. Si${\displaystyle B}$es una rama que contiene un literal${\displaystyle L}$, y${\displaystyle C}$es una cláusula cuya expansión viola la regularidad, entonces${\displaystyle C}$contiene${\displaystyle L}$. Para cerrar el cuadro, es necesario expandir y cerrar, entre otras, la rama donde${\displaystyle B-L}$, dónde${\displaystyle L}$ocurre dos veces. Sin embargo, las fórmulas en esta rama son exactamente las mismas que las fórmulas de${\displaystyle B}$solos. Como resultado, los mismos pasos de expansión que cierran${\displaystyle B-L}$también cerca${\displaystyle B}$Esto significa que la expansión${\displaystyle C}$era innecesario; además, si${\displaystyle C}$Al contener otros literales, su expansión generó 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 del tableau debido a algunas unificaciones; sin embargo, estas pueden combinarse con las sustituciones utilizadas para cerrar el resto del tableau.

Un método para evitar que las fórmulas que hacen referencia a mundos diferentes interactúen de forma incorrecta consiste en asegurarse de que todas las fórmulas de una rama hagan referencia al mismo mundo. Esta condición se cumple inicialmente, ya que se asume que todas las fórmulas del conjunto que se va a comprobar hacen referencia al mismo mundo. Al expandir una rama, pueden darse dos situaciones: que las nuevas fórmulas hagan referencia al mismo mundo que las demás de la rama o que 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 aún son relativas al mundo anterior.

Como ejemplo, en S5 cada fórmula${\displaystyle \Box A}$que es cierto en un mundo también es cierto en todos los mundos accesibles (es decir, en todos los mundos accesibles ambos${\displaystyle A}$y${\displaystyle \Box A}$son ciertas). Por lo tanto, al aplicar${\displaystyle {\frac {\neg \Box B}{\neg B}}}$, cuya consecuencia se mantiene en un mundo diferente, se eliminan todas las fórmulas de la rama, pero se pueden conservar todas las fórmulas${\displaystyle \Box A}$, ya que esto también se aplica al nuevo mundo. Para mantener la exhaustividad, las fórmulas eliminadas se añaden a todas las demás ramas que aún hacen referencia al viejo mundo.

Otro mecanismo para asegurar 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${\displaystyle A}$, uno escribiría${\displaystyle w:A}$para dejarlo explícito que${\displaystyle A}$se mantiene en el mundo${\displaystyle w}$.

Todas las reglas de expansión proposicional se adaptan a esta variante al establecer que todas se refieren a fórmulas con la misma etiqueta de mundo. Por ejemplo,${\displaystyle w:A\land B}$genera dos nodos etiquetados con${\displaystyle w:A}$y${\displaystyle w:B}$; una rama se cierra solo si contiene dos literales opuestos del mismo mundo, como${\displaystyle w:a}$y${\displaystyle w:\neg a}$; no se genera ningún cierre si las dos etiquetas de mundo son diferentes, como en${\displaystyle w:a}$y${\displaystyle w':\neg a}$.

Una regla de expansión modal puede tener una consecuencia que se refiere a mundos diferentes. Por ejemplo, la regla para${\displaystyle \neg \Box A}$se escribiría de la siguiente manera

${\displaystyle {\frac {w:\neg \Box A}{w':\neg A}}}$

La condición previa y el consecuente de esta regla se refieren a mundos.${\displaystyle w}$y${\displaystyle w'}$, respectivamente. Los distintos cálculos utilizan diferentes métodos para controlar la accesibilidad de los mundos utilizados como etiquetas. Algunos incluyen pseudofórmulas como${\displaystyle wRw'}$para indicar que${\displaystyle w'}$es accesible desde${\displaystyle w}$. Otros utilizan secuencias de enteros como etiquetas del mundo, esta notación representa implícitamente la relación de accesibilidad (por ejemplo,${\displaystyle (1,4,2,3)}$es accesible desde${\displaystyle (1,4,2)}$.)

El problema de la interacción entre fórmulas que existen en mundos diferentes puede superarse utilizando diagramas de conjuntos etiquetados. Estos 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 tableaux 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${\displaystyle S}$ellos comprueban la existencia de un modelo${\displaystyle M}$y un mundo${\displaystyle w}$de tal manera que${\displaystyle M,w\models S}$.

Las reglas de expansión dependen de la lógica modal particular utilizada. Un sistema de tableau para la lógica modal básica K se puede obtener agregando a las reglas de tableau proposicionales la siguiente:

${\displaystyle (K){\frac {\Box A_{1};\ldots$ ;\Box A_{n};\neg \Box B}{A_{1};\ldots ;A_{n};\neg B}}}

Intuitivamente, la condición previa de esta regla expresa la verdad de todas las fórmulas.${\displaystyle A_{1},\ldots ,A_{n}}$en todos los mundos accesibles y la verdad de${\displaystyle \neg B}$en algunos mundos accesibles. La consecuencia de esta regla es una fórmula que debe ser verdadera en uno de esos mundos donde${\displaystyle \neg B}$Es cierto.

En términos más técnicos, los métodos de tablas modales comprueban la existencia de un modelo.${\displaystyle M}$y un mundo${\displaystyle w}$que hacen que un conjunto de fórmulas sea verdadero. Si${\displaystyle \Box A_{1};\ldots$ ;\Box A_{n};\neg \Box B} son verdaderas en${\displaystyle w}$, debe haber un mundo${\displaystyle w'}$que es accesible desde${\displaystyle w}$y eso hace${\displaystyle A_{1};\ldots ;A_{n};\neg B}$verdadero. Por lo tanto, esta regla equivale a derivar un conjunto de fórmulas que deben cumplirse en tales${\displaystyle w'}$.

Si bien las condiciones previas${\displaystyle \Box A_{1};\ldots$ ;\Box A_{n};\neg \Box B} se suponen satisfechos por${\displaystyle M,w}$las consecuencias${\displaystyle A_{1};\ldots ;A_{n};\neg B}$se supone que se satisfacen en${\displaystyle M,w'}$Mismo modelo, pero posiblemente mundos diferentes. Los tableaux etiquetados con conjuntos no registran explícitamente el mundo en el que se asume que cada fórmula es verdadera: dos nodos pueden o no referirse al mismo mundo. Sin embargo, se asume que las fórmulas que etiquetan cualquier nodo son verdaderas en el mismo mundo.

Debido a la posible existencia de mundos distintos donde se asumen ciertas fórmulas, 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 cambio de un mundo a otro. Esta condición se captura automáticamente mediante los tableaux de etiquetado de conjuntos, dado que las reglas de expansión se basan únicamente en la hoja donde se aplican y no en sus ancestros.

Notablemente,${\displaystyle (K)}$no se extiende directamente a múltiples fórmulas en recuadro negadas como en${\displaystyle \Box A_{1};\ldots$ ;\Box A_{n};\neg \Box B_{1};\neg \Box B_{2}} : mientras exista un mundo accesible donde${\displaystyle B_{1}}$es falso y uno en el que${\displaystyle B_{2}}$Es falso, estos dos mundos no son necesariamente iguales.

A diferencia de las reglas proposicionales,${\displaystyle (K)}$establece condiciones sobre todas sus precondiciones. Por ejemplo, no se puede aplicar a un nodo etiquetado por${\displaystyle a;\Box b;\Box (b\to c);\neg \Box c}$; mientras que este conjunto es inconsistente y esto podría probarse fácilmente aplicando${\displaystyle (K)}$Esta regla no se puede aplicar debido a la fórmula.${\displaystyle a}$, lo cual ni siquiera es relevante para la inconsistencia. La eliminación de tales fórmulas es posible gracias a la regla:

${\displaystyle (\theta ){\frac {A_{1};\ldots ;A_{n};B_{1};\ldots ;B_{m}}{A_{1};\ldots ;A_{n}}}}$

La adición de esta regla (regla de adelgazamiento) hace que el cálculo resultante no sea confluente: puede ser imposible cerrar un tableau para un conjunto inconsistente, incluso si existe un tableau cerrado para el mismo conjunto.

Regla${\displaystyle (\theta )}$Es no determinista: el conjunto de fórmulas que se deben eliminar (o conservar) puede elegirse arbitrariamente; esto genera 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 resulten inaplicables. Tener un gran número de opciones posibles dificulta el problema de buscar un tableau cerrado.

Este no determinismo puede evitarse restringiendo el uso de${\displaystyle (\theta )}$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 hacían que la regla anterior fuera inaplicable. Este mecanismo para eliminar${\displaystyle (\theta )}$Se ha demostrado que preserva la completitud para muchas lógicas modales.

El axioma T expresa la reflexividad de la relación de accesibilidad: todo mundo es accesible desde sí mismo. La regla de expansión de tableau correspondiente es:

${\displaystyle (T){\frac {A_{1};\ldots ;A_{n};\Box B}{A_{1};\ldots ;A_{n};\Box B;B}}}$

Esta regla relaciona condiciones sobre el mismo mundo: si${\displaystyle \Box B}$es cierto en un mundo, por reflexividad${\displaystyle B}$Esto también es cierto 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${\displaystyle \Box B}$desde la precondición hasta el consecuente, a pesar de que esta fórmula se haya "utilizado" para generar${\displaystyle B}$Esto es correcto, ya que el mundo considerado es el mismo, por lo tanto${\displaystyle \Box B}$También se cumple allí. Esta "copia" es necesaria en algunos casos. Es necesario, por ejemplo, para probar la inconsistencia de ${\displaystyle \Box (a\land \neg \Box a)}$: las únicas reglas aplicables son las siguientes${\displaystyle (T),(\land ),(\theta ),(K)}$, de la cual uno queda bloqueado si${\displaystyle \Box a}$no se copia.

Un método diferente para tratar las fórmulas que se mantienen en mundos alternativos es comenzar un tablero diferente para cada nuevo mundo que se introduce en el tablero. Por ejemplo,${\displaystyle \neg \Box A}$implica que${\displaystyle A}$es falso en un mundo accesible, por lo que se comienza un nuevo cuadro enraizado por${\displaystyle \neg A}$Este nuevo tableau se adjunta al nodo del tableau original donde se ha aplicado la regla de expansión; el cierre de este tableau genera inmediatamente el cierre de todas las ramas donde se encuentra ese nodo, independientemente de si el mismo nodo está asociado a otros tableaux auxiliares. Las reglas de expansión para los tableaux auxiliares son las mismas que para el original; por lo tanto, un tableau auxiliar puede tener a su vez otros tableaux (sub)auxiliares.

Los cuadros modales anteriores establecen la consistencia de un conjunto de fórmulas y pueden utilizarse para resolver el problema de la consecuencia lógica local . Este es el problema de determinar si, para cada modelo${\displaystyle M}$, si${\displaystyle A}$es cierto en un mundo${\displaystyle w}$, entonces${\displaystyle B}$Esto también es cierto en el mismo mundo. Esto es lo mismo que comprobar si${\displaystyle B}$es cierto en un mundo de un modelo, bajo el supuesto de que${\displaystyle A}$Esto también es cierto en el mismo mundo del mismo modelo.

Un problema relacionado es el problema de la consecuencia global, donde se supone que una fórmula (o conjunto de fórmulas)${\displaystyle G}$es cierto en todos los mundos posibles del modelo. El problema es el de comprobar si, en todos los modelos${\displaystyle M}$dónde${\displaystyle G}$es cierto en todos los mundos,${\displaystyle B}$Esto también es cierto en todos los mundos.

Las suposiciones locales y globales difieren en los modelos donde la fórmula supuesta es verdadera en algunos mundos pero no en otros. Como ejemplo,${\displaystyle \{P,\neg \Box (P\land Q)\}}$implica${\displaystyle \neg \Box Q}$globalmente pero no localmente. La implicación local no se cumple en un modelo que consta de dos mundos haciendo${\displaystyle P}$y${\displaystyle \neg P,Q}$verdadero, respectivamente, y donde el segundo es accesible desde el primero; en el primer mundo, las suposiciones son verdaderas pero${\displaystyle \neg \Box Q}$es falso. Este contraejemplo funciona porque${\displaystyle P}$puede asumirse verdadero en un mundo y falso en otro. Sin embargo, si la misma suposición se considera global,${\displaystyle \neg P}$No está permitido en ningún mundo del modelo.

Estos dos problemas se pueden combinar, de modo que se pueda comprobar si${\displaystyle B}$es una consecuencia local de${\displaystyle A}$bajo el supuesto global${\displaystyle G}$. Los tableaux calculati pueden manejar la suposición global mediante una regla que permite agregarla a cada nodo, independientemente del mundo al que se refiera.

Al escribir reglas de expansión de tablas, las fórmulas a menudo se denotan utilizando una convención, de modo que, por ejemplo, α siempre se considera que es${\displaystyle \alpha _{1}\land \alpha _{2}}$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 demás columnas. Una fórmula con línea superior, como por ejemplo:${\displaystyle {\overline {\alpha _{1}}}}$indica que${\displaystyle \alpha _{1}}$es la negación de cualquier fórmula que aparezca en su lugar, de modo que, por ejemplo, en la fórmula${\displaystyle \neg (a\lor b)}$la subfórmula${\displaystyle \alpha _{1}}$es la negación de un .

Dado que cada etiqueta indica muchas fórmulas equivalentes, esta notación permite escribir una única regla para todas ellas. Por ejemplo, la regla de expansión de conjunciones se formula como:

${\displaystyle (\alpha ){\frac {\alpha }{\begin{array}{c}\alpha _{1}\\\alpha _{2}\end{array}}}}$