Method of analytic tableaux

In proof theory, the semantic tableau^[1] (/tæˈbloʊ,ˈtæbloʊ/; plural: tableaux), also called an analytic tableau,^[2]truth tree,^[1] or simply tree,^[2] is a decision procedure for sentential and related logics, and a proof procedure for formulae of first-order logic.^[1] An analytic tableau is a tree structure computed for a logical formula, having at each node a subformula of the original formula to be proved or refuted. Computation constructs this tree and uses it to prove or refute the whole formula.^[3] The tableau method can also determine the satisfiability of finite sets of formulas of various logics. It is the most popular proof procedure for modal logics.^[4]

A method of truth trees contains a fixed set of rules for producing trees from a given logical formula, or set of logical formulas. Those trees will have more formulas at each branch, and in some cases, a branch can come to contain both a formula and its negation, which is to say, a contradiction. In that case, the branch is said to close.^[1] If every branch in a tree closes, the tree itself is said to close. In virtue of the rules for construction of tableaux, a closed tree is a proof that the original formula, or set of formulas, used to construct it was itself self-contradictory,^[1] and therefore false. Conversely, a tableau can also prove that a logical formula is tautologous: if a formula is tautologous, its negation is a contradiction, so a tableau built from its negation will close.^[1]

In his Symbolic Logic Part II, Charles Lutwidge Dodgson (also known by his literary pseudonym, Lewis Carroll) introduced the Method of Trees, the earliest modern use of a truth tree.^[5]

El método de los tableaux semánticos fue inventado independientemente por el lógico holandés Evert Willem Beth (Beth 1955), ^{[ 6 ]} el lógico y filósofo finlandés Jaakko Hintikka y el filósofo sueco Stig Kanger, ^{[ 7 ]} y simplificado, para la lógica clásica, por Raymond Smullyan (Smullyan 1968, 1995). ^{[ 8 ]} La simplificación de Smullyan, los "tableaux unilaterales", se describe aquí. El método de Smullyan ha sido generalizado a lógicas proposicionales y de primer orden arbitrarias y multivaluadas por Walter Carnielli (Carnielli 1987). ^{[ 9 ]}

Los tableaux pueden verse intuitivamente como sistemas secuenciales invertidos. Esta relación simétrica entre tableaux y sistemas secuenciales se estableció formalmente en (Carnielli 1991). ^{[ 10 ]}

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

${\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 , implicación , disyunción y conjunción . ${\displaystyle \neg }$${\displaystyle \to }$${\displaystyle \lor }$${\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 implican si es insatisfacible. ${\displaystyle A_{1},\ldots ,A_{n}}$${\displaystyle B}$${\displaystyle \{A_{1},\ldots ,A_{n},\neg B\}}$

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

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

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 y ; ^{[ 13 ]}${\displaystyle {\boldsymbol {\mathsf {T}}}(X)}$${\displaystyle {\boldsymbol {\mathsf {T}}}(Y)}$
• ${\displaystyle {\boldsymbol {\mathsf {F}}}(X\land Y)}$, crea dos hijos hermanos de su hoja, que contienen las fórmulas y respectivamente; ^{[ 14 ]}${\displaystyle {\boldsymbol {\mathsf {F}}}(X)}$${\displaystyle {\boldsymbol {\mathsf {F}}}(Y)}$
• ${\displaystyle {\boldsymbol {\mathsf {T}}}(X\lor Y)}$, crea dos hijos hermanos de su hoja, que contienen las fórmulas y respectivamente;${\displaystyle {\boldsymbol {\mathsf {T}}}(X)}$${\displaystyle {\boldsymbol {\mathsf {T}}}(Y)}$
• ${\displaystyle {\boldsymbol {\mathsf {F}}}(X\lor Y)}$, añade a su hoja la cadena de dos nodos que contienen las fórmulas y ;${\displaystyle {\boldsymbol {\mathsf {F}}}(X)}$${\displaystyle {\boldsymbol {\mathsf {F}}}(Y)}$
• ${\displaystyle {\boldsymbol {\mathsf {T}}}(X\to Y)}$, crea dos hijos hermanos de su hoja, que contienen las fórmulas y respectivamente;${\displaystyle {\boldsymbol {\mathsf {F}}}(X)}$${\displaystyle {\boldsymbol {\mathsf {T}}}(Y)}$
• ${\displaystyle {\boldsymbol {\mathsf {F}}}(X\to Y)}$, añade a su hoja la cadena de dos nodos que contienen las fórmulas y ;${\displaystyle {\boldsymbol {\mathsf {T}}}(X)}$${\displaystyle {\boldsymbol {\mathsf {F}}}(Y)}$
• ${\displaystyle {\boldsymbol {\mathsf {T}}}(\neg X)}$, agregar 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 primitiva sino que la definen en términos de implicación y falsedad ( ), las reglas de tableau para se reemplazan por ${\displaystyle \neg \Phi \,{\overset {\text{def}}{=}}\,\Phi \to \bot }$${\displaystyle \neg }$

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 (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 pueden considerarse conjuntivas, ya que tanto como están implícitas al ser verdaderas. Las fórmulas de tipo beta pueden considerarse disyuntivas, ya que o está implícita al ser verdaderas. Las tablas siguientes muestran cómo determinar el tipo y los componentes de cualquier fórmula proposicional dada . ^{[ 15 ]}${\displaystyle \alpha }$${\displaystyle \beta }$${\displaystyle \alpha _{1},\alpha _{2}}$${\displaystyle \beta _{1},\beta _{2}}$${\displaystyle \alpha _{1}}$${\displaystyle \alpha _{2}}$${\displaystyle \alpha }$${\displaystyle \beta _{1}}$${\displaystyle \beta _{2}}$${\displaystyle \beta }$

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 tableau proposicional usando la notación anterior, siempre que se encuentra una fórmula de tipo alfa, sus dos componentes se agregan a la rama actual que se está expandiendo. Siempre que se encuentra 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. ^{[ 16 ]}${\displaystyle \alpha _{1},\alpha _{2}}$${\displaystyle \theta }$${\displaystyle \theta }$${\displaystyle \theta }$${\displaystyle \beta _{1}}$${\displaystyle \theta }$${\displaystyle \beta _{2}}$

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 con el conjunto que contiene tanto como en su lugar. En particular, si una hoja está etiquetada con , se le puede agregar un nodo con la etiqueta : ${\displaystyle A\land B}$${\displaystyle A}$${\displaystyle B}$${\displaystyle X\cup \{A\land B\}}$${\displaystyle X\cup \{A,B\}}$

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

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. ${\displaystyle X\cup \{A\lor B\}}$${\displaystyle X\cup \{A\}}$${\displaystyle X\cup \{B\}}$

${\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 , y dadas anteriormente son suficientes para decidir si un conjunto dado de fórmulas en forma normal negada son conjuntamente satisfacibles: ${\displaystyle (\land )}$${\displaystyle (\lor )}$${\displaystyle (id)}$${\displaystyle X'}$

Simplemente aplicamos todas las reglas posibles en todos los órdenes posibles hasta que encontremos un tableau cerrado para o hasta que agotemos todas las posibilidades y concluyamos que cada tableau para es abierto. ${\displaystyle X'}$${\displaystyle X'}$

En el primer caso, es conjuntamente insatisfacible, y en el segundo, el nodo hoja de la rama abierta asigna a las fórmulas atómicas y a las fórmulas atómicas negadas, lo que la hace conjuntamente satisfacible. La lógica clásica posee la interesante propiedad de que solo necesitamos analizar completamente un tableau: si se cierra, es insatisfacible, y si se abre, es satisfacible. Sin embargo, esta propiedad no suele estar presente en otras lógicas. ${\displaystyle X'}$${\displaystyle X'}$${\displaystyle X'}$${\displaystyle X'}$

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 plantear esta cuestión, se puede comprobar si la fórmula A es una tautología de la lógica clásica: ${\displaystyle X=\{\neg A\}}$

Si el tableau 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 tableau abierto para da una asignación que falsifica A.${\displaystyle \{\neg A\}}$${\displaystyle \neg A}$${\displaystyle \{\neg A\}}$

Los tableaux se extienden a la lógica de predicados de primer orden mediante dos reglas para tratar los cuantificadores universales y existenciales, respectivamente. Se pueden utilizar dos conjuntos de reglas diferentes; ambos emplean una forma de skolemización para manejar los cuantificadores existenciales, pero difieren en el tratamiento de los cuantificadores universales.

Se supone que el conjunto de fórmulas que se utilizan para comprobar su validez no contiene variables libres; esto no supone una limitación, ya que las variables libres se cuantifican universalmente de forma implícita, por lo que se pueden añadir cuantificadores universales a 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: ${\displaystyle \forall x.\gamma (x)}$${\displaystyle \gamma (t)}$${\displaystyle t}$

${\displaystyle (\forall ){\frac {\forall x.\gamma (x)}{\gamma (t)}}}$donde es un término fundamental arbitrario${\displaystyle t}$

A diferencia de las reglas para los conectores proposicionales, pueden ser necesarias múltiples aplicaciones de esta regla a la misma fórmula. Por ejemplo, el conjunto solo puede demostrarse insatisfacible si tanto como se generan a partir de . ${\displaystyle \{\neg P(a)\lor \neg P(b),\forall x.P(x)\}}$${\displaystyle P(a)}$${\displaystyle P(b)}$${\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 genera su skolemización , donde es un nuevo símbolo constante. ${\displaystyle \exists x.\delta (x)}$${\displaystyle \delta (c)}$${\displaystyle c}$

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

El término de Skolem es una constante (una función de aridad 0) porque la cuantificación sobre no se produce dentro del alcance de ningún cuantificador universal. Si la fórmula original contenía cuantificadores universales tales que la cuantificación sobre estuviera dentro de su alcance, estos cuantificadores han sido evidentemente eliminados al aplicar la regla de los cuantificadores universales. ${\displaystyle c}$${\displaystyle x}$${\displaystyle x}$

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 se puede generar incluso si no estaba en la fórmula original, sino que es una constante de Skolem creada por la regla para cuantificadores existenciales. ${\displaystyle \forall y.\gamma (y)}$${\displaystyle \gamma (c)}$${\displaystyle c}$

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. Por ejemplo, el conjunto es insatisfacible, pero nunca se obtiene un tableau cerrado si se sigue aplicando imprudentemente la regla para cuantificadores universales a , generando, por ejemplo , . Siempre se puede encontrar un tableau cerrado descartando esta y otras políticas similares "injustas" de aplicación de las reglas del tableau. ${\displaystyle \{\neg P(f(c)),\forall x.P(x)\}}$${\displaystyle \forall x.P(x)}$${\displaystyle P(c),P(f(c)),P(f(f(c))),\ldots }$

La regla para cuantificadores universales 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 limitá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. ${\displaystyle (\forall )}$

El principal problema de un tableau sin unificación radica en cómo elegir un término base para la regla del cuantificador universal. Si bien se puede utilizar cualquier término base posible, es evidente que la mayoría resultaría inútil para cerrar el tableau. ${\displaystyle t}$

Una solución a este problema consiste en "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 lograr 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: ${\displaystyle \forall x.\gamma (x)}$${\displaystyle \gamma (x')}$${\displaystyle x'}$

${\displaystyle (\forall ){\frac {\forall x.\gamma (x)}{\gamma (x')}}}$¿Dónde hay una variable que no aparece en ningún otro lugar del tableau?${\displaystyle x'}$

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.

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

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 no tienen por qué 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. En consecuencia, una fórmula como puede estar dentro del ámbito 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 x.\delta (x)}$

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

Esta regla incorpora una simplificación respecto a una regla donde son las variables libres de la rama, no de por sí solas. Esta regla puede simplificarse aún más mediante la reutilización de un símbolo de función si ya se ha utilizado en una fórmula idéntica, salvo por el cambio de nombre de las variables. ${\displaystyle x_{1},\ldots ,x_{n}}$${\displaystyle \delta }$${\displaystyle \delta }$

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 se cuantifican universalmente. Todos estos cuantificadores abarcan la fórmula completa. En otras palabras, si es la fórmula obtenida al separar la conjunción de las fórmulas de cada rama, y ​​son las variables libres en ella, entonces es la fórmula representada por el tableau. Se aplican las siguientes consideraciones: ${\displaystyle F}$${\displaystyle x_{1},\ldots ,x_{n}}$${\displaystyle \forall x_{1},\ldots ,x_{n}.F}$

• 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: puesto que significa que es verdadero para cada valor posible de , entonces es verdadero para el término que el unificador más general reemplaza con .${\displaystyle \gamma (x')}$${\displaystyle \gamma }$${\displaystyle x'}$${\displaystyle \gamma (t)}$${\displaystyle t}$${\displaystyle x}$
• 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 y , donde es libre en ambos, la fórmula representada por el tableau es algo de la forma . Esta fórmula implica que es verdadera para cualquier valor de , pero no implica en general que para dos términos diferentes y , ya que estos dos términos pueden tomar valores diferentes. Esto significa que no puede ser reemplazada por dos términos diferentes en y .${\displaystyle A(x)}$${\displaystyle B(x)}$${\displaystyle x}$${\displaystyle \forall x.(...A(x)...B(x)...)}$${\displaystyle (...A(x)...B(x)...)}$${\displaystyle x}$${\displaystyle (...A(t)...A(t')...)}$${\displaystyle t}$${\displaystyle t'}$${\displaystyle x}$${\displaystyle A(x)}$${\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 sobre el recíproco de la fórmula, pero aún tratan las variables libres como cuantificadas universalmente. Por ejemplo, no es válido (no es verdadero en el modelo donde , y la interpretación donde ). En consecuencia, es satisfacible (es satisfecha por el mismo modelo e interpretación). Sin embargo, se podría generar un tableau cerrado con y , y sustituir con generaría un cierre. Un procedimiento correcto es hacer explícitos primero los cuantificadores universales, generando así .${\displaystyle P(x)\to P(c)}$${\displaystyle D=\{1,2\},P(1)=\bot ,P(2)=\top ,c=1}$${\displaystyle x=2}$${\displaystyle \{P(x),\neg P(c)\}}$${\displaystyle P(x)}$${\displaystyle \neg P(c)}$${\displaystyle x}$${\displaystyle c}$${\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".

Un cálculo de tableaux es un conjunto de reglas que permite construir y modificar un tableaux. Las reglas de tableaux proposicionales, las reglas de tableaux sin unificación y las reglas de tableaux con unificación son todos cálculos de tableaux. Algunas propiedades importantes que un cálculo de tableaux 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 en tablas para cualquier conjunto de fórmulas insatisfacibles. Los cálculos de tablas mencionados anteriormente pueden demostrarse completos.

Una diferencia notable entre el cálculo de tableau con unificación y los otros dos métodos radica en que estos últimos solo modifican un tableau añadiéndole nuevos nodos, mientras que el primero permite sustituciones para modificar la parte existente del tableau. En términos generales, los cálculos de tableau se clasifican como destructivos o no destructivos según si solo añaden nuevos nodos al tableau o no. Por lo tanto, el cálculo de tableau con unificación es destructivo, mientras que el tableau proposicional y el tableau sin unificación son no destructivos.

La confluencia de pruebas es la propiedad de un cálculo de tableaux que permite obtener una prueba para un conjunto insatisfacible arbitrario a partir de un tableaux arbitrario, suponiendo que este tableaux se haya obtenido aplicando las reglas del cálculo. En otras palabras, en un cálculo de tableaux con confluencia de pruebas, a partir de un conjunto insatisfacible se puede aplicar cualquier conjunto de reglas y aun así obtener un tableaux a partir del cual se puede obtener uno cerrado aplicando otras reglas.

Un cálculo de tableaux es simplemente un conjunto de reglas que prescribe cómo se puede modificar un tableaux. Un procedimiento de prueba es un método para encontrar una prueba (si existe). En otras palabras, un cálculo de tableaux 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 insatisfacible. Por ejemplo, es insatisfacible, pero tanto los tableaux con unificación como los tableaux sin unificación permiten que la regla para los cuantificadores universales se aplique repetidamente a la última fórmula, mientras que simplemente aplicar la regla de disyunción a la tercera conduciría directamente al cierre. ${\displaystyle \{P(f(c)),R(c),\neg P(f(c))\lor \neg R(c),\forall x.Q(x)\}}$

Para los procedimientos de demostración, se ha definido la completitud de la siguiente manera: un procedimiento es fuertemente completo si permite hallar un tableau cerrado para cualquier conjunto insatisfacible de fórmulas. La confluencia de la demostración del cálculo subyacente es relevante para la completitud: la confluencia de la demostración garantiza que siempre se puede generar un tableau cerrado a partir de un tableau parcialmente construido arbitrario (si el conjunto es insatisfacible). Sin la confluencia de la demostración, la aplicación de una regla «incorrecta» puede resultar en la imposibilidad de completar el tableau aplicando otras reglas.

Los tableaux proposicionales y los tableaux sin unificación poseen procedimientos de prueba fuertemente completos. En particular, un procedimiento de prueba completo consiste en aplicar las reglas de manera justa . Esto se debe a que la única forma en que dichos cálculos no pueden generar un tableau cerrado a partir de un conjunto insatisfacible es no aplicando algunas reglas pertinentes.

Para los tableaux proposicionales, la equidad implica expandir cada fórmula en cada rama. Más precisamente, para cada fórmula y cada rama en la que se encuentra, se ha utilizado la regla que tiene la fórmula como precondición para expandir la rama. Un procedimiento de prueba equitativo para tableaux proposicionales es fuertemente completo.

Para los tableaux de primer orden sin unificación, la condición de equidad es similar, con la excepción de que la regla para los cuantificadores universales podría requerir más de una aplicación. La equidad equivale a expandir cada cuantificador universal infinitamente. En otras palabras, una política de aplicación de reglas equitativa 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 tablas es completo, todo conjunto insatisfacible de fórmulas tiene asociado un tablero cerrado. Si bien este tablero siempre se puede obtener aplicando algunas de las reglas del cálculo, persiste el problema de determinar qué reglas aplicar para una fórmula dada. En consecuencia, la completitud no implica automáticamente la existencia de una política factible de aplicación de reglas que siempre conduzca a un tablero cerrado para todo conjunto insatisfacible de fórmulas. Si bien un procedimiento de prueba justo es completo para el tablero básico y el tablero sin unificación, esto no ocurre con el tablero con unificación.

Una solución general para este problema consiste en buscar en el espacio de tableaux hasta encontrar uno cerrado (si existe alguno, es decir, el conjunto es insatisfacible). En este enfoque, se parte de un tableau vacío y se aplican recursivamente todas las reglas posibles. Este procedimiento recorre un árbol (implícito) cuyos nodos están etiquetados con tableaux, de manera que el tableau de un nodo se obtiene a partir del tableau de su nodo padre mediante la aplicación de una de las reglas válidas.

Dado que cada rama puede ser infinita, este árbol debe recorrerse en amplitud en lugar de 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 espacio polinomial, es recorrerlos en profundidad con profundización iterativa : primero se recorre el árbol en profundidad hasta cierta profundidad, luego se aumenta la profundidad y se realiza la visita nuevamente. Este procedimiento particular utiliza la profundidad (que también es el número de reglas de tableau que se han aplicado) para decidir cuándo detenerse en cada paso. En su lugar, se han utilizado otros parámetros (como el tamaño del tableau que etiqueta un nodo).

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 opción posible; sin embargo, la completitud no se ve afectada, ya que la segunda rama se seguirá expandiendo si la primera se cierra finalmente. Por ejemplo, un tableau con raíz , hijo , y dos hojas y puede cerrarse de dos maneras: aplicando primero a y luego a , o viceversa. Claramente no es necesario seguir ambas posibilidades; se puede considerar solo el caso en el que se aplica primero a y descartar el caso en el que se aplica primero a . Esta es una restricción global porque lo que permite ignorar esta segunda expansión es la presencia del otro tableau, donde la expansión se aplica primero a y después a . ${\displaystyle \neg a\land \neg b}$${\displaystyle a\lor b}$${\displaystyle a}$${\displaystyle b}$${\displaystyle (\land )}$${\displaystyle a}$${\displaystyle b}$${\displaystyle (\land )}$${\displaystyle a}$${\displaystyle b}$${\displaystyle a}$${\displaystyle b}$

Cuando se aplican a conjuntos de cláusulas (en lugar de fórmulas arbitrarias), los métodos de tableaux permiten varias 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 a menudo se omiten para mayor claridad, de modo que, por ejemplo, en realidad significa . Nótese que, si se toman literalmente, estas dos fórmulas no son lo mismo que para la satisfacibilidad: más bien, la satisfacibilidad es la misma que la de . Que las variables libres se cuantifiquen universalmente no es una consecuencia de la definición de satisfacibilidad de primer orden; más bien se utiliza como una suposición común implícita al tratar con cláusulas. ${\displaystyle \forall x_{1},\ldots ,x_{n}L_{1}\lor \cdots \lor L_{m}}$${\displaystyle L_{i}}$${\displaystyle P(x,y)\lor Q(f(x))}$${\displaystyle \forall x,y.P(x,y)\lor Q(f(x))}$${\displaystyle P(x,y)\lor Q(f(x))}$${\displaystyle \exists x,y.P(x,y)\lor Q(f(x))}$

Las únicas reglas de expansión aplicables a una cláusula son y ; estas dos reglas pueden sustituirse por su combinación sin perder completitud. En particular, la siguiente regla corresponde a la aplicación secuencial de las reglas y del cálculo de primer orden con unificación. ${\displaystyle (\forall )}$${\displaystyle (\lor )}$${\displaystyle (\forall )}$${\displaystyle (\lor )}$

${\displaystyle (C){\frac {L_{1}\lor \cdots \lor L_{n}}{L_{1}'|\cdots |L_{n}'}}}$donde se obtiene reemplazando cada variable con una nueva en${\displaystyle L_{1}'\lor \cdots \lor L_{n}'}$${\displaystyle L_{1}\lor \cdots \lor L_{n}}$

Cuando el conjunto que se va a comprobar para comprobar su satisfacibilidad está compuesto únicamente por cláusulas, esto y las reglas de unificación son suficientes para probar la insatisfacibilidad. En otras palabras, el tableau calculi compuesto por y es completo. ${\displaystyle (C)}$${\displaystyle (\sigma )}$

Dado que la regla de expansión de cláusulas solo genera literales y nunca cláusulas nuevas, solo se puede aplicar a las cláusulas del conjunto de entrada. Por lo tanto, la regla de expansión de cláusulas se puede restringir aún más al caso en que la cláusula esté presente en el conjunto de entrada.

${\displaystyle (C){\frac {L_{1}\lor \cdots \lor L_{n}}{L_{1}'|\cdots |L_{n}'}}}$donde se obtiene reemplazando cada variable con una nueva en , que es una cláusula del conjunto de entrada${\displaystyle L_{1}'\lor \cdots \lor L_{n}'}$${\displaystyle L_{1}\lor \cdots \lor L_{n}}$

Dado que esta regla explota directamente las cláusulas del conjunto de entrada, no es necesario inicializar el tableau con la cadena de cláusulas de entrada. Por lo tanto, el tableau inicial puede inicializarse con el único nodo etiquetado ; esta etiqueta suele omitirse por ser implícita. Como resultado de esta simplificación adicional, cada nodo del tableau (excepto la raíz) se etiqueta con un literal. ${\displaystyle true}$

Se pueden utilizar diversas optimizaciones para la tabla de cláusulas. Estas optimizaciones tienen como objetivo reducir el número de tablas posibles que se deben explorar al buscar una tabla cerrada, tal como se describe en la sección anterior "Búsqueda de una tabla cerrada".

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 tableau formado 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 tableaux tiene cuatro hojas en general, pero solo una si se impone la conectividad. Esto significa que la conectividad deja solo un tableau para intentar expandir, en lugar de los cuatro que se pueden considerar en general. 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. ${\displaystyle true-a}$${\displaystyle \{a,\neg a\lor b,\neg c\lor d,\neg b\}}$${\displaystyle \neg a\lor b}$

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

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.

Estos pasos de expansión no permitidos son, sin embargo, inútiles. Si es una rama que contiene un literal y es una cláusula cuya expansión viola la regularidad, entonces contiene . Para cerrar el tableau, 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 por sí solas. 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 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. ${\displaystyle B}$${\displaystyle L}$${\displaystyle C}$${\displaystyle C}$${\displaystyle L}$${\displaystyle B-L}$${\displaystyle L}$${\displaystyle B}$${\displaystyle B-L}$${\displaystyle B}$${\displaystyle C}$${\displaystyle C}$

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 solo condiciones sobre un mundo posible, sino también sobre aquellos que son accesibles desde él. Por ejemplo, es verdadero en un mundo si es verdadero en todos los mundos que son accesibles desde él. ${\displaystyle \Box A}$${\displaystyle A}$

En cuanto a la lógica proposicional, los diagramas para lógicas modales se basan en la descomposición recursiva de fórmulas en sus componentes básicos. Sin embargo, expandir una fórmula modal puede requerir establecer condiciones sobre diferentes mundos. Por ejemplo, si es verdadera en un mundo, entonces existe un mundo accesible desde él donde es falsa. No obstante, no se puede simplemente añadir la siguiente regla a las proposicionales. ${\displaystyle \neg \Box A}$${\displaystyle A}$

${\displaystyle {\frac {\neg \Box A}{\neg A}}}$

En los tableaux 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 afirma que es verdadera en el mundo actual y es falsa en un mundo accesible desde él. Simplemente aplicando y la regla de expansión anterior se obtendrían y , pero estas dos fórmulas no deberían generar una contradicción en general, ya que se cumplen en mundos diferentes. Los tableaux modales calculan reglas del tipo de la anterior, pero incluyen mecanismos para evitar la interacción incorrecta de fórmulas que se refieren a mundos diferentes. ${\displaystyle a\land \neg \Box a}$${\displaystyle a}$${\displaystyle a}$${\displaystyle (\land )}$${\displaystyle a}$${\displaystyle \neg a}$

Técnicamente, los tableaux para lógicas modales comprueban la satisfacibilidad de un conjunto de fórmulas: verifican si existe un modelo y un mundo tales que las fórmulas del conjunto sean verdaderas en ese modelo y mundo. En el ejemplo anterior, mientras que establece la verdad de en , la fórmula establece la verdad de en algún mundo accesible desde y que, en general, puede ser diferente de . Los tableaux calculi para lógica modal tienen en cuenta que las fórmulas pueden referirse a mundos diferentes. ${\displaystyle M}$${\displaystyle w}$${\displaystyle a}$${\displaystyle a}$${\displaystyle w}$${\displaystyle \neg \Box a}$${\displaystyle \neg a}$${\displaystyle w'}$${\displaystyle w}$${\displaystyle w}$

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 cual es cierto para la mayoría de las lógicas modales. Si este es el caso, una fórmula como es verdadera si existe un sucesor donde se cumple y un sucesor donde se cumple. A la inversa, si se puede demostrar la insatisfacibilidad de en un sucesor arbitrario, la fórmula se demuestra insatisfacible sin comprobar los mundos donde se cumple. Al mismo tiempo, si se puede demostrar la insatisfacibilidad de , no hay necesidad de comprobar . Como resultado, aunque hay dos maneras posibles de expandir , una de estas dos maneras siempre es suficiente para probar la insatisfacibilidad si la fórmula es insatisfacible. Por ejemplo, se puede expandir el tableau 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 insatisfacibilidad no pueda probarse de esta manera, y que en su lugar se debiera haber considerado el mundo donde se cumple. En consecuencia, siempre se puede probar la insatisfacibilidad expandiendo solo o solo; sin embargo, si se elige incorrectamente, el tableau resultante puede no ser cerrado. Expandir cualquiera de las subfórmulas conduce a cálculos de tableau que son completos pero no confluentes en cuanto a la prueba. Por lo tanto, puede ser necesario realizar la búsqueda descrita en "Búsqueda de un tableau cerrado". ${\displaystyle \neg \Box A\land \neg \Box B}$${\displaystyle \neg A}$${\displaystyle \neg B}$${\displaystyle \neg A}$${\displaystyle \neg B}$${\displaystyle \neg B}$${\displaystyle \neg A}$${\displaystyle \neg \Box A\land \neg \Box B}$${\displaystyle \neg A}$${\displaystyle \neg B}$${\displaystyle \neg \Box A}$${\displaystyle \neg \Box B}$

Dependiendo de si la precondición y la consecuencia de una regla de expansión de tableau se refieren al mismo mundo o no, la regla se denomina estática o transaccional. Si bien las reglas para conectores proposicionales son todas estáticas, no todas las reglas para conectores modales son transaccionales: por ejemplo, en toda lógica modal que incluya el axioma T , se cumple que implica en el mismo mundo. En consecuencia, la regla de expansión de tableau relativa (modal) es estática, ya que tanto su precondición como su consecuencia se refieren al mismo mundo. ${\displaystyle \Box A}$${\displaystyle A}$

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.

Por ejemplo, en S5, toda fórmula que es verdadera en un mundo también lo es en todos los mundos accesibles (es decir, en todos los mundos accesibles, tanto como son verdaderas). Por lo tanto, al aplicar , cuya consecuencia se mantiene en un mundo diferente, se eliminan todas las fórmulas de la rama, pero se conservan todas las fórmulas , ya que estas también se mantienen en el nuevo mundo. Para mantener la completitud, las fórmulas eliminadas se añaden a todas las demás ramas que aún hacen referencia al mundo anterior. ${\displaystyle \Box A}$${\displaystyle A}$${\displaystyle \Box A}$${\displaystyle {\frac {\neg \Box B}{\neg B}}}$${\displaystyle \Box A}$

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 , se escribiría para dejar explícito que se cumple en el mundo . ${\displaystyle A}$${\displaystyle w:A}$${\displaystyle A}$${\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, 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 . ${\displaystyle w:A\land B}$${\displaystyle w:A}$${\displaystyle w:B}$${\displaystyle w:a}$${\displaystyle w:\neg a}$${\displaystyle w:a}$${\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 se escribiría de la siguiente manera: ${\displaystyle \neg \Box A}$

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

La precondición y el consecuente de esta regla se refieren a los mundos y , respectivamente. Los distintos cálculos utilizan diferentes métodos para controlar la accesibilidad de los mundos utilizados como etiquetas. Algunos incluyen pseudofórmulas como para indicar que es accesible desde . Otros utilizan secuencias de enteros como etiquetas de mundo, representando esta notación implícitamente la relación de accesibilidad (por ejemplo, es accesible desde ). ${\displaystyle w}$${\displaystyle w'}$${\displaystyle wRw'}$${\displaystyle w'}$${\displaystyle w}$${\displaystyle (1,4,2,3)}$${\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 , comprueban la existencia de un modelo y un mundo tales que . ${\displaystyle S}$${\displaystyle M}$${\displaystyle w}$${\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 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. ${\displaystyle A_{1},\ldots ,A_{n}}$${\displaystyle \neg B}$${\displaystyle \neg B}$

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 existir un mundo que sea accesible desde y que haga que sea verdadero. Por lo tanto, esta regla equivale a derivar un conjunto de fórmulas que deben satisfacerse en dicho . ${\displaystyle M}$${\displaystyle w}$${\displaystyle \Box A_{1};\ldots ;\Box A_{n};\neg \Box B}$${\displaystyle w}$${\displaystyle w'}$${\displaystyle w}$${\displaystyle A_{1};\ldots ;A_{n};\neg B}$${\displaystyle w'}$

Si bien se asume que las precondiciones se cumplen en , se asume que las consecuencias se cumplen en : mismo modelo, pero posiblemente mundos diferentes. Los tableaux etiquetados con conjuntos no registran explícitamente el mundo donde 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 dado son verdaderas en el mismo mundo. ${\displaystyle \Box A_{1};\ldots ;\Box A_{n};\neg \Box B}$${\displaystyle M,w}$${\displaystyle A_{1};\ldots ;A_{n};\neg B}$${\displaystyle M,w'}$

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.

Cabe destacar que no se extiende directamente a múltiples fórmulas en caja negadas como en : si bien existe un mundo accesible donde es falso y otro en el que es falso, estos dos mundos no son necesariamente el mismo. ${\displaystyle (K)}$${\displaystyle \Box A_{1};\ldots ;\Box A_{n};\neg \Box B_{1};\neg \Box B_{2}}$${\displaystyle B_{1}}$${\displaystyle B_{2}}$

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

${\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.

La regla no es determinista: el conjunto de fórmulas que se deben eliminar (o conservar) puede elegirse arbitrariamente; esto plantea el problema de elegir un conjunto de fórmulas a 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. Un gran número de opciones posibles dificulta la búsqueda de un tableau cerrado. ${\displaystyle (\theta )}$

Este no determinismo puede evitarse restringiendo su uso para que solo se aplique antes de una regla de expansión modal y para que solo elimine las fórmulas que invalidan dicha regla. Esta condición también puede formularse fusionando ambas reglas en una sola. La regla resultante produce el mismo resultado que la anterior, pero descarta implícitamente todas las fórmulas que invalidaban la regla anterior. Se ha demostrado que este mecanismo de eliminación preserva la completitud en muchas lógicas modales. ${\displaystyle (\theta )}$${\displaystyle (\theta )}$

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 es verdadera en un mundo, por reflexividad también lo es 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. ${\displaystyle \Box B}$${\displaystyle B}$

Esta regla copia de la precondición al consecuente, a pesar de que esta fórmula se haya "usado" 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. Es necesario, por ejemplo, para probar la inconsistencia de : las únicas reglas aplicables están en orden , de las cuales uno queda bloqueado si no se copia. ${\displaystyle \Box B}$${\displaystyle B}$${\displaystyle \Box B}$${\displaystyle \Box (a\land \neg \Box a)}$${\displaystyle (T),(\land ),(\theta ),(K)}$${\displaystyle \Box a}$

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

Los diagramas 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 problema consiste en determinar si, para cada modelo , si es verdadera en un mundo , entonces también lo es en el mismo mundo. Esto equivale a comprobar si es verdadera en un mundo de un modelo, bajo el supuesto de que también lo es en el mismo mundo del mismo modelo. ${\displaystyle M}$${\displaystyle A}$${\displaystyle w}$${\displaystyle B}$${\displaystyle B}$${\displaystyle A}$

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

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

Estos dos problemas pueden combinarse, de modo que se puede comprobar si es una consecuencia local de bajo la suposición global . Los cálculos de tableaux pueden abordar la suposición global mediante una regla que permite su adición a cada nodo, independientemente del mundo al que se refiera. ${\displaystyle B}$${\displaystyle A}$${\displaystyle G}$

En ocasiones 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 igual a . La siguiente tabla proporciona la notación para fórmulas en lógica proposicional, de primer orden y modal. ${\displaystyle \alpha _{1}\land \alpha _{2}}$

Cada etiqueta de la primera columna se considera una fórmula de las demás columnas. Una fórmula tachada, como indica que es la negación de cualquier fórmula que aparezca en su lugar, de modo que, por ejemplo, en la fórmula, la subfórmula es la negación de una . ${\displaystyle {\overline {\alpha _{1}}}}$${\displaystyle \alpha _{1}}$${\displaystyle \neg (a\lor b)}$${\displaystyle \alpha _{1}}$

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}}}}$

• Resolución (lógica)

• Beth, Evert W. (1955). "Vinculación semántica y derivabilidad formal" . Mededelingen van de Koninklijke Nederlandse Akademie van Wetenschappen, Afdeling Letterkunde . 18 (13): 309–42 .Reimpreso en Intikka, Jaakko, ed. (1969). La filosofía de las matemáticas . Oxford University Press. ISBN 978-0-19-875011-6.
• Bostock, David (1997). Lógica intermedia . Oxford University Press. ISBN 978-0-19-156707-0.
• Carnielli, Walter A. (1987). " Sistematización de lógicas multivaluadas finitas mediante el método de tableaux" . The Journal of Symbolic Logic . 52 (2): 473– 493. doi : 10.2307/2274395 . JSTOR  2274395. S2CID  42822367 .
• Carnielli, Walter A. (1991). "Sobre secuencias y diagramas para lógicas multivaluadas" (PDF) . The Journal of Non-Classical Logics . 8 (1): 59– 76. Archivado del original (PDF) el 5 de marzo de 2016. Recuperado el 11 de octubre de 2014 .
• D'Agostino, M.; Gabbay, D .; Haehnle, R.; Posegga, J., eds. (1999). Manual de métodos de Tableau . Kluwer. ISBN 978-94-017-1754-0.
• Fitting, Melvin (1996) [1990]. Lógica de primer orden y demostración automática de teoremas (2.ª ed.). Nueva York: Springer. doi : 10.1007/978-1-4612-2360-3 . ISBN 978-1-4612-7515-2. S2CID  10411039 .
• Girle, Rod (2014). Lógicas modales y filosofía (2.ª ed.). Taylor & Francis. ISBN 978-1-317-49217-7.
• Goré, Rajeev. "Métodos de Tableau para lógicas modales y temporales". Manual de métodos de Tableau . págs.  297–396 .
• Hähnle, Reiner (2001). «3. Tableaux and Related Methods» . En Robinson, Alan JA; Voronkov, Andrei (eds.). Handbook of Automated Reasoning . Elsevier. pp.  101–179 . ISBN 978-0-08-053279-0.
• Howson, Colin (11 de octubre de 2005) [1997]. Lógica con árboles: una introducción a la lógica simbólica . Routledge. ISBN 978-1-134-78550-6.
• Jarmużek, Tomasz (2020). Hartman, Jan (ed.). «Métodos de tableau para la lógica proposicional y la lógica de términos» (PDF) . Serie: Estudios en filosofía, historia de las ideas y sociedades modernas . 20. Traducido por Jaskólski, Sławomir. Berlín, Berna, Bruselas, Nueva York, Oxford, Varsovia, Viena: Peter Lang : 228. doi : 10.3726/b18008 . ISBN 9783631846537ISSN 2191-1878​ ​
• Jeffrey, Richard (2006) [1967]. Lógica formal: su alcance y límites (4.ª ed.). Hackett. ISBN 978-0-87220-813-1.
• Letz, Reinhold; Stenz, Gernot. "28. Eliminación de modelos y procedimientos de conexión de tablas". Manual de razonamiento automatizado . págs.  2015–2114 .
• Robinson, John Alan ; Voronkov, Andrei , eds. (2001). Manual de razonamiento automatizado . Vol. 1. MIT Press . pp. 203 y ss. ISBN 0444829490.
• Smullyan, Raymond (1995) [1968]. Lógica de primer orden . Dover. ISBN 978-0-486-68370-6.
• Smullyan, Raymond (2014). Guía para principiantes de lógica matemática . Dover. ISBN 978-0486492377.
• La Enciclopedia de Filosofía, ed. (11 de diciembre de 2023). "Lógica moderna: el período booleano: Carroll" . La Enciclopedia de Filosofía . Consultado el 26 de diciembre de 2023 .
• Zeman, Joseph Jay (1973). Lógica modal: Los sistemas modales de Lewis . Clarendon Press. ISBN 978-0-19-824374-8OCLC 641504​ ​

• TABLEAUX : una conferencia internacional anual sobre razonamiento automatizado con tableaux analíticos y métodos relacionados.
• JAR : Revista de Razonamiento Automatizado
• El paquete tableaux : un demostrador interactivo para lógica proposicional y de primer orden que utiliza tableaux.
• Generador de pruebas de árbol : otro demostrador interactivo para lógica proposicional y de primer orden que utiliza tableaux.
• LoTREC : un demostrador genérico basado en tableaux para lógicas modales de IRIT/Universidad de Toulouse.
• Introducción a Truth Trees en YouTube