Método dos Tableaux Analíticos

Na teoria da prova, o tableau semântico (pronúncia em francês: ​[ta'blo]; singular: tableau; plural: tableaux), também chamado de árvore verdade, é um sistema de dedução para resolver problemas de decisão na lógica proposicional e outras relacionadas, e um procedimento de prova para fórmulas da lógica de primeira ordem. O método de tableau também pode determinar a satisfatibilidade para conjuntos finitos de fórmulas de várias lógicas. É o mais popular procedimento de prova para a lógica modal (Girle 2000), além de adequado para implementações em computadores. O método dos tableaux semântico foi inventada pelo lógico holandês Evert Willem Beth (Beth 1955), e, de forma independente, pelo lógico finlandês Jaakko Hintikka, foi simplificado para a lógica clássica por Raymond Smullyan (Smullyan 1968, 1995). A simplificação de Smullyan, "one-sided tableaux", é descrito a seguir. O método de Smullyan foi generalizado para arbitrárias lógicas proposicionais polivalentes e de primeira ordem por Walter Carnielli (Carnielli 1987). O tableaux pode ser intuitivamente visto como o método de sequentes de cima para baixo. Esta relação simétrica entre o tableaux e o cálculo de sequentes foi formalmente estabelecido por Carnielli (1991).

Um tableau analítica tem, para cada nó, um subformula da fórmula na origem. Em outras palavras, é um tableau que satisfaz a propriedade da subformula.

Introdução

Para refutar um tableaux, é necessário mostrar que a negação de uma fórmula não pode ser satisfeita. Existem regras para a manipulação de cada um dos  conectivos habituais, começando principalmente pelo conjuntivo. Em muitos casos, a aplicação destas regras faz com que o sub-tableau se divida em dois. Quantificadores são instanciados. Se qualquer ramo de um tableau leva a uma evidente contradição, o ramo fecha. Se todos os ramos se fecham, a prova está completa e a fórmula original é uma verdade lógica.

Embora a idéia fundamental por trás do método do tableau analítico ser derivado do teorema da eliminação do corte da teoria da prova estrutural, as origens do cálculo de tableau se encontra no significado (ou semântica) dos conectivos lógicos, assim como a conexão com a teoria da prova feita apenas nas últimas décadas.

Mais especificamente, um cálculo de tableau consiste de uma coleção finita de regras, cada regra especificando como quebrar uma conectivo lógica em suas partes constituintes. As regras são normalmente expressas em termos de conjuntos finitos de fórmulas, apesar de haver uma lógica para a qual devemos usar estruturas de dados mais complicadas, tais como multiconjuntos, listas, ou até mesmo árvores de fórmulas. De agora em diante, "conjunto" denota qualquer um {conjunto, multiconjunto, lista ou árvore}.

Se há uma regra para cada conectivo lógico, então, o processo vai, eventualmente, produzir um conjunto que consiste apenas de fórmulas atômicas, e os seus opostos, que não pode ser decomposto. Tal conjunto é facilmente reconhecível como satisfatível ou insatisfatível com respeito à semântica da lógica em questão. Para acompanhar este processo, os nós de um tableau em si são definidos na forma de uma árvore e os galhos desta árvore são criados e avaliados de forma sistemática. Como um método sistemático para procurar esta árvore dá origem a um algoritmo para a realização de dedução e raciocínio automatizado. Note que esta árvore maior está presente, independentemente, dos nós conterem conjuntos, multisets, listas e árvores.

Lógica proposicional

Esta seção apresenta o cálculo de tableau para a lógica proposicional clássica. Um tableau verifica se um determinado conjunto de fórmulas é satisfatível ou não. Ele pode ser usado para verificar a validade ou vínculo: uma fórmula é tautologia se a sua negação é insatisfatível. As fórmulas $A_{1},\ldots ,A_{n}$ implicam em $B$ se $\{A_{1},\ldots ,A_{n},\neg B\}$ é insatisfatível.

O maior princípio do tableaux proposicional é tentar "quebrar" um complexo de fórmulas em menores, até pares complementares de literais serem produzidos ou não ser possível continuar a expansão.

Tableau inicial para o conjunto {(a⋁¬b)⋀b,¬a}

O método funciona em uma árvore cujos nós são rotulados com fórmulas. Em cada etapa, esta árvore é modificada; no caso proposicional, a única alteração permitida é a adição de nós como descendentes de uma folha. O procedimento inicia-se por gerar a árvore feita de uma cadeia de todas as fórmulas do conjunto para provar sua insatisfatibilidade. Uma variante para este passo inicial é começar com um único nó de árvore, cuja raiz é rotulado por $\top$; neste segundo caso, o procedimento pode sempre copiar uma fórmula no conjunto abaixo de uma folha. Como exemplo, o tableau para o conjunto $\{(a\vee \neg b)\wedge b,\neg a\}$ é mostrado.

O princípio do tableau é que as fórmulas do nós do mesmo ramo são considerados em conjunto, enquanto os diferentes ramos são considerados disjuntos. Como resultado, um tableau é uma árvore como representação de uma fórmula que é uma disjunção de conjunções. Essa fórmula é equivalente a definida para provar sua insatisfatibilidade. O procedimento modifica o tableau de tal forma que a fórmula representada pelo tableau resultante é equivalente ao original. Uma dessas conjunções podem conter um par de literais complementares, caso em que o conjunção é provado ser insatisfatível. Se todas as conjunções são provadas como insatisfativeis, o conjunto original de fórmulas é insatisfatível.

Conjunção

((a⋁¬b)⋀b) gera (a⋁¬b) e (b)

Sempre que um ramo de um tableau contém uma fórmula $A\wedge B$ que é a conjunção de duas fórmulas, essas duas fórmulas são consequências dessa fórmula. Este fato pode ser formalizado mediante a seguinte regra para a expansão de um tableau:

$(\land )$ Se um ramo do tableau contém uma fórmula conjuntiva $A\land B$, adicionar a sua folha uma cadeia de dois nós que contém as fórmulas $A$ e $B$

Esta regra é geralmente escrita como segue:

$(\land ){\frac {A\wedge B}{\begin{array}{c}A\\B\end{array}}}$

Uma variante desta regra permite que um nó contenha um conjunto de fórmulas, em vez de um único. Neste caso, as fórmulas deste conjunto são considerados uma conjunção, assim, pode-se adicionar $\{A,B\}$ no final de um ramo que contém $A\wedge B$. Mais precisamente, se um nó em um ramo é rotulado $X\cup \{A\wedge B\}$ pode-se juntar ao ramo da nova folha $X\cup \{A,B\}$.

Disjunção

(a⋁¬b) gera (a) e (¬b)

Se um ramo de um tableau contém uma fórmula que é uma disjunção de duas fórmulas, tais como $A\vee B$ a seguinte regra pode ser aplicada:

$(\lor )$ Se um nó em um ramo contém uma fórmula disjuntiva $A\lor B$, em seguida, cria-se dois filhos para a folha do ramo, contendo $A$ e $B$, respectivamente.

Esta regra divide um ramo em dois, diferindo apenas para o nó final. Desde que os ramos sejam levados como disjunção para o outro, os dois ramos resultantes são equivalentes a um original, como a disjunção dos nós não comuns é precisamente $A\vee B$. A regra de disjunção é, em geral, formalmente escrita usando o símbolo $|$ para separar as fórmulas dos dois nós distintos a ser criado:

$(\vee ){\frac {A\vee B}{A|B}}$

Se nós, presume-se que contenham um conjuntos de fórmulas, esta regra é substituída pelo seguinte: se um nó é rotulado $Y\cup \{A\vee B\}$, em uma folha do ramo, podem ser acrescentados dois nós filhos rotulados $Y\cup \{A\}$ e $Y\cup \{B\}$, respectivamente.

Negação

O objetivo do tableaux é gerar progressivamente fórmulas mais simples até que os pares de literais opostos sejam produzidos, ou nenhuma outra regra possa ser aplicada. A negação pode ser tratada por, inicialmente, montar fórmulas na forma normal da negação, de modo que a negação ocorre apenas na frente de literais. Alternativamente, pode-se usar leis De Morgan durante a expansão do tableau, de modo que, por exemplo, $\neg (A\wedge B)$ é tratado como $\neg A\vee \neg B$. Regras para introduzir ou remover um par de opostos (como em $\neg \neg A$) também são usados neste caso (caso contrário, não haveria nenhuma forma de expansão de uma fórmula como $\neg \neg (A\wedge B)$:

$(\neg 1){\frac {A}{\neg \neg A}}$

$(\neg 2){\frac {\neg \neg A}{A}}$

O tableau é fechado

Fechamento

Cada tableau pode ser considerado como uma representação gráfica de uma fórmula, a qual é equivalente ao tableau construído a partir dele. Esta fórmula é a seguinte: cada ramo do tableau representa o conjunto de suas fórmulas; o tableau representa a disjunção de seus ramos. As regras de expansão transformam um tableau em uma fórmula equivalentemente representada. O tableau é inicializado com um único ramo que contém as fórmulas do conjunto de entrada, todos os tableaux subsequentes obtidos a partir das fórmulas representadas são equivalentes a esse conjunto (na variante em que o inicial do tableau é o único nó rotulado como verdadeiro, as fórmulas representadas por tableaux são consequências do conjunto original.)

Um tableau para um conjunto satisfatível {a⋀c,¬a⋁b}: todas as regras foram aplicadas para cada fórmula em todos os ramos, mas o quadro não é fechado (somente o ramo esquerdo é fechado), como esperado para conjuntos satisfativeis

O método dos tableaux trabalha começando com o conjunto inicial de fórmulas, e em seguida, adiciona ao tableau mais simples, fórmulas mais simples até que a contradição seja mostrada na forma de literais oposto. Desde que a fórmula representada por um tableau seja a disjunção das fórmulas representadas por seus ramos, a contradição é obtida quando cada ramo contém um par de literais opostos.

Uma vez que um ramo contém um literal e a sua negação, a sua respectiva fórmula é insatisfatível. Como resultado, o ramo pode agora ser "fechado", como não há necessidade de expandir ainda mais. Se todos os ramos de um tableau são fechados, a fórmula representada pelo tableau é insatisfatível; portanto, o conjunto original é insatisfatível. A obtenção de um quadro onde todos os ramos estão fechados é uma maneira para provar a insatisfatibilidade do conjunto original. No caso proposicional, pode-se também provar a satisfatibilidade pela impossibilidade de encontrar um tableau fechado, desde que cada expansão da regra tenha sido aplicada em todo lugar que poderia ser aplicada. Em particular, se um tableau contém algum ramo aberto (não-fechado) e cada fórmula que não é literal, tenha sido utilizada por uma regra para gerar um novo nó em cada ramo em que a fórmula se encontra, o conjunto é satisfatível.

Esta regra leva em conta que uma fórmula pode ocorrer em mais de um ramo (este é o caso, se existe pelo menos um ponto de ramificação "abaixo" do nó). Neste caso, a regra para expandir a fórmula tem que ser aplicada de modo que a sua conclusão(s) sejam acrescentadas para todos esses ramos que ainda estão em aberto, assim pode-se concluir que o tableau não pode ser ampliado ainda mais, e que a fórmula, portanto, é satisfatível.

Tableau conjunto-marcado

Uma variante do tableau que toma como base marcar nós com conjuntos de fórmulas, em vez de simples fórmulas. Neste caso, o tableau inicial é um único nó marcado com o conjunto-marcado para ser provado como satisfatório. As fórmulas de um conjunto, são, portanto, consideradas em conjunto.

As regras de expansão do tableau podem agora trabalhar apenas nas folhas do tableau, ignorando todos os nós internos. Para a conjunção, a regra é baseada na equivalência de um conjunto contendo um conjunção $A\wedge B$ com o conjunto que contém tanto $A$ e $B$ no lugar dele. Em particular, se uma folha é marcada com $X\cup \{A\wedge B\}$ um nó pode ser acrescentado a ele com a marcação $X\cup \{A,B\}$:

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

Para a disjunção, um conjunto $X\cup \{A\vee B\}$ é equivalente a disjunção de dois conjuntos $X\cup \{A\}$ e $X\cup \{B\}$. Como resultado, se o primeiro conjunto marcado for uma folha, dois filhos podem ser acrescentados, marcado com as duas últimas fórmulas.

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

Finalmente, se um conjunto contém um literal e a sua negação, este ramo pode ser fechado:

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

Um tableau para um determinado conjunto finito X é uma (de cabeça para baixo) árvore finita com raiz X em que todos os nós filhos são obtidos aplicando-se as regras de tableau em seus pais. Um ramo de tal tableau é fechado se o nó folha está "fechado" (com literais opostos). Um tableau é fechado se todos os seus ramos estão fechados. Um tableau é aberto se, pelo menos, um ramo não é fechado.

Aqui estão dois tableaux fechado para o conjunto X = {r0 & ~r0, p0 & ((~p0 ∨ q0) & ~q0)} com cada regra de aplicação no lado direito (& e ~ significa $\land$ e $\neg$, respectivamente).

 {r0 & ~r0, p0 & ((~p0 v q0) & ~q0)}                              {r0 & ~r0, p0 & ((~p0 v q0) & ~q0)}
--------------------------------------(&)          ------------------------------------------------------------(&)
{r0, ~r0, p0 & ((~p0 v q0) & ~q0)}                                {r0 & ~r0, p0, ((~p0 v q0) & ~q0)}
-------------------------------------(id)           ----------------------------------------------------------(&)
              fechado                                                {r0 & ~r0, p0, (~p0 v q0), ~q0}
                                                  -------------------------------------------------------------(v)
                                                          {r0 & ~r0, p0, ~p0, ~q0} | {r0 & ~r0, p0, q0, ~q0}
                                                      -------------------------- (id) ---------------------- (id)
                                                                 fechado                       fechado

O lado esquerdo fecha depois de apenas uma regra de aplicação, enquanto o lado direito erra o alvo e leva muito mais tempo para fechar. Claramente, preferimos sempre encontrar o menor tableaux fechado, mas também pode ser demonstrado que um único algoritmo que encontra o menor fechado tableaux para todos os conjuntos de entrada de fórmulas, não pode existir.

As três regras $(\wedge )$, $(\vee )$ e $(id)$ dadas acima são suficientes para decidir se um determinado conjunto de $X'$ das fórmulas na forma normal da negação conjuntamente satisfatível:

Basta aplicar todas as regras possíveis em todas as ordens possíveis, até encontrar um tableau fechado para $X'$ ou até esgotar todas as possibilidades e concluir que cada tableau para $X'$ está aberto.

No primeiro caso, $X'$ é co-insatisfatível e no segundo caso o nó folha do ramo aberto dá uma atribuição para a fórmulas atômica e fórmulas atômicas negadas que faz $X'$ um conjunto satisfatível. A lógica clássica, na verdade, tem muitas propriedades agradáveis que precisamos investigar somente um tableau completamente: se fechado, então, $X'$ é insatisfatível e se ele estiver aberto, então, $X'$ é satisfatível. Mas essa propriedade não é geralmente apreciada por outras lógicas.

Estas regras são suficientes para toda a lógica clássica tomando um conjunto inicial de fórmulas X, e substituindo cada membro C , por sua logicamente equivalente na forma normal da negação C' dando um conjunto de fórmulas, X' . Sabemos que X é satisfatível se e somente se X' é satisfatível, então basta procurar um tableau fechado para X' , usando o procedimento descrito acima.

Por definição $X=\{\neg A\}$ podemos testar se a fórmula A é uma tautologia da lógica clássica:

Se o tableau para $\{\neg A\}$ fecha-se, então, $\neg A$ é insatisfatível e então A é uma tautologia, pois nenhuma atribuição de valores de verdade nunca vai fazer A falso. Caso contrário, qualquer folha de qualquer ramo de qualquer tableau para $\{\neg A\}$ dá uma atribuição que A se torna falso.

Condicional

Na lógica clássica proposicional geralmente tem uma conectivo para indicar o condicional material. Se nós escrevemos este conjuntivo como ⇒ e, em seguida, a fórmula de A ⇒ B significa "se A então B". É possível dar uma regra de tableau para quebrar A ⇒ B em seu constituinte de fórmulas. Da mesma forma, podemos dar uma regra cada para quebrar cada um (A ∧ B), (A ∨ B), (A) e (A ⇒ B). Juntas, essas regras dão uma procedimento terminal para decidir se um determinado conjunto de fórmulas é, simultaneamente, satisfatível na lógica clássica, pois cada regra quebra uma fórmula em seus constituintes, mas nenhuma regra cria fórmulas maiores de menores constituintes. Temos assim que, eventualmente, chegar a um nó que contém apenas átomos e negações de átomos. Se este último nó corresponde a (id) em seguida, podemos fechar o ramo, caso contrário, ele permanece aberto.

Mas observe que as seguintes equivalências mantidas na lógica clássica, onde ( ... ) = ( ... ) significa que o lado esquerdo fórmula é logicamente equivalente ao lado direito da fórmula:

${\begin{array}{lcl}\neg (A\land B)&=&\neg A\lor \neg B\\\neg (A\lor B)&=&\neg A\land \neg B\\\neg (\neg A)&=&A\\\neg (A\Rightarrow B)&=&A\land \neg B\\A\Rightarrow B&=&\neg A\lor B\\A\Leftrightarrow B&=&(A\land B)\lor (\neg A\land \neg B)\\\neg (A\Leftrightarrow B)&=&(A\land \neg B)\lor (\neg A\land B)\end{array}}$

Se começamos com uma fórmula arbitrária C da lógica clássica, e aplicarmos essas equivalências repetidamente para substituir os lados a esquerda com os lados a direita de C, então, iremos obter uma fórmula C' , que é logicamente equivalente a C, mas que tem a propriedade de que C' não contém implicações, e aparece na frente de fórmulas atômicas. Tal fórmula é dita estar em forma normal da negação e é possível provar formalmente que cada fórmula C da lógica clássica tem uma fórmula logicamente equivalente C' na forma normal da negação. Isto é, C é satisfatível se e somente se C' é satisfatível.

Tableau na lógica de primeira ordem

Tableaux são estendidos para a lógica de predicados de primeira ordem por duas regras para lidar com os quantificadores universais e existenciais, respectivamente. Dois conjuntos diferentes de regras podem ser utilizados; ambos utilizam uma forma normal de Skolem para tratamento de quantificadores existenciais, mas diferem no tratamento dos quantificadores universais.

O conjunto de fórmulas para verificar a validade não deveria conter variáveis livres, isso não é uma limitação, como variáveis livres são implicitamente universalmente quantificadas, então quantificadores universal sobre estas variáveis podem ser adicionados, resultando em uma fórmula sem variáveis livres.

Tableau de primeira ordem sem unificação

Uma fórmula de primeira ordem $\forall x.\gamma (x)$ implica todas as fórmulas $\gamma (t)$ onde $t$ é um termo básico. A seguinte regra de inferência é, portanto, correta:

$(\forall ){\frac {\forall x.\gamma (x)}{\gamma (t)}}$ onde $t$ é termo básico arbitrário.

Contrariando as regras para os conectivos proposicionais, várias aplicações desta regra para a mesma fórmula pode ser necessário. Como exemplo, o conjunto $\{\neg P(a)\vee \neg P(b),\forall x.P(x)\}$ só pode ser provado insatisfatível se tanto $P(a)$ e $P(b)$ são gerados a partir de $\forall x.P(x)$.

Quantificadores existencial são tratados por meio de Skolemização. Em particular, uma fórmula com um quantificador existencial lider, como $\exists x.\delta (x)$ gera a forma Skolem $\delta (c)$, onde $c$ é um novo símbolo de constante.

$(\exists ){\frac {\exists x.\delta (x)}{\delta (c)}}$ onde $c$ é um nova constante

Um tableau sem unificação para {∀x.P(x), ∃x.(P(x)⋁P(f(x)))}. Para maior clareza, as fórmulas são numeradas a esquerda, e a fórmula e a regra utilizada em cada etapa a direita

O termo Skolem $c$ é uma constante (uma função de aridade 0), pois a quantificação sobre $x$ não ocorrer dentro do escopo de qualquer quantificador universal. Se a fórmula original continha alguns quantificadores universal de tal forma que a quantificação sobre $x$ foi dentro de seu âmbito de aplicação, estes quantificadores têm, evidentemente, sido removido por aplicação da regra universal de quantificadores.

A regra para os quantificadores existenciais apresentar um novo símbolo de constante. Esse símbolo pode ser usado pela regra de quantificadores universias, de modo que $\forall y.\gamma (y)$ pode gerar $\gamma (c)$ mesmo se $c$ não for um fórmula original, mas é um constante Skolem criada pela regra de quantificadores existenciais.

As duas regras acima para o quantificadores universais e existenciais são corretas, e por isso são regras proposicionais: se um conjunto de fórmulas, gera um tableau fechado, este conjunto é insatisfatível. A integralidade também pode ser provada: se um conjunto de fórmulas é insatisfatível, existe um tableau fechado construído por estas regras. No entanto, na verdade, encontrar um tableau fechado requer uma adequada política de aplicação das regras. Caso contrário, um conjunto insatisfatível pode gerar um tableau de crescimento infinito. Como exemplo, o conjunto $\{\neg P(f(c)),\forall x.P(x)\}$ é insatisfatível, mas um tableau fechado nunca é obtido se, imprudentemente, aplicar a regra de quantificadores universais para $\forall x.P(x)$, gerando, por exemplo, $P(c),P(f(c)),P(f(f(c))),\ldots$. Um tableau fechado pode ser sempre encontrado por exclusão deste e similares políticas "injustas" de aplicação das regras de tableau.

A regra de quantificadores universais $(\forall )$ é a única regra não-determinística, pois não especifica qual o prazo para instanciar. Além disso, enquanto as outras regras devem ser aplicadas apenas uma vez para cada fórmula e cada caminho é a fórmula, este pode exigir várias aplicações. A aplicação desta regra pode, no entanto, ser restringido por adiar a aplicação da regra até que nenhuma outra regra aplicável e restringindo a aplicação da regra para os termos básicos que já aparecem no caminho do tableau. A variante de tableaux com a unificação mostrado abaixo visa resolver o problema não-determinismo.

Tableau de primeira ordem com unificação

O principal problema do tableau sem união é como escolher um termo básico $t$ para a regra do quantificador universal. De fato, todos os possíveis termos básicos podem ser usados, mas é claro que a maioria deles pode ser inútil para fechar o tabuleiro.

Uma solução para este problema é "atrasar" a escolha do termo para o tempo quando a consequência da regra permite o fechamento de pelo menos um ramo do tableau. Isso pode ser feito usando uma variável em vez de um termo, de modo que $\forall x.\gamma (x)$ gera $\gamma (x')$ e, em seguida, permitindo substituições para, mais tarde, substituir $x'$ com um termo. A regra para os quantificadores universais torna-se:

$(\forall ){\frac {\forall x.\gamma (x)}{\gamma (x')}}$ onde $x'$ é uma variável que não ocorre em qualquer outro lugar do tableau

Enquanto o conjunto inicial de fórmulas é suposto que não contêm variáveis livres, uma fórmula do tableau conter as variáveis livres geradas por esta regra. Estas variáveis livres são implicitamente consideradas universalmente quantificadas.

Esta regra utiliza uma variável em vez de um termo básico. O ganho dessa alteração é que, essas variáveis podem ser, então, dadas um valor, quando um ramo de um tableau pode ser fechado, a solução do problema de geração de termos que podem ser inúteis.

$(\sigma )$ se $\sigma$ é o unificador mais geral de dois literais $A$ e $B$, onde $A$ e a negação de $B$ ocorrer no mesmo ramo do tableau, $\sigma$ pode ser aplicado ao mesmo tempo, para todas as fórmulas do tableau

Como um exemplo, $\{\neg P(a),\forall x.P(x)\}$ pode ser provado como insatisfatível pela primeira geração de $P(x_{1})$; a negação deste literal é unificável com $\neg P(a)$, o unificador mais geral que é a substituição que substitui $x_{1}$ com $a$; aplicar esta substituição resulta na substituição de $P(x_{1})$ com $P(a)$, que fecha o tableau.

Esta regra fecha, pelo menos, um ramo de um tableau, o que contém o par considerado de literais. No entanto, a substituição tem de ser aplicado a todos no tableau, não só nestes dois literais. Isto é expresso ao dizer que as variáveis livres do tableau são rígida: se uma ocorrência de uma variável é substituída por outra coisa, todas as outras ocorrências da mesma variável deve ser substituído da mesma forma. Formalmente, as variáveis livres são (implicitamente) universalmente quantificadas e todas as fórmulas do tableau estão dentro do escopo desses quantificadores.

Quantificadores existenciais, são tratados por Skolemização. Ao contrário do tableau sem unificação, termos Skolem não podem ser simples e constantes. De fato, as fórmulas em um tableau com a unificação pode conter variáveis livres, que são implicitamente consideradas universalmente quantificadas. Como resultado, uma fórmula como $\exists x.\delta (x)$ pode estar dentro do escopo de quantificadores universais; se este for o caso, o termo Skolem não é uma simples constante, mas um termo de um novo símbolo de função e as variáveis livres da fórmula.

$(\exists ){\frac {\exists x.\delta (x)}{\delta (f(x_{1},\ldots ,x_{n}))}}$ onde $f$ é um novo símbolo de função e $x_{1},\ldots ,x_{n}$ as variáveis livres de $\delta$

Um tableau de primeira ordem com a unificação de {∀x.P(x), ∃x.(P(x)⋁P(f(x)))}. Para maior clareza, as fórmulas são numeradas da esquerda e a fórmula e a regra utilizada em cada etapa é o da direita

Esta regra incorpora um simplificação de mais de uma regra onde $x_{1},\ldots ,x_{n}$ são as variáveis livres do ramo, e não de $\delta$ sozinhos. Esta regra pode ser ainda mais simplificadas por reutilização de um símbolo de função, caso já tenha sido usada em uma fórmula, que é idêntico a $\delta$ até mudar o nome da variável.

A fórmula representada por um tableau é obtida de forma semelhante para o caso proposicional, com a suposição adicional de que variáveis livres são consideradas universalmente quantificadas. Como para o caso proposicional, fórmulas em cada ramo são conjugados e as fórmulas resultantes são desassociadas. Além disso, todas as variáveis livres da fórmula resultante são universalmente quantificadas. Todos estes quantificadores têm toda a fórmula no seu âmbito. Em outras palavras, se $F$ é a fórmula obtida separando o conjunto das fórmulas em cada ramo, e $x_{1},\ldots ,x_{n}$ são as variáveis livres, então $\forall x_{1},\ldots ,x_{n}.F$ é a fórmula representada pelo tableau. As seguintes considerações se aplicam:

• A suposição de que variáveis livres são universalmente quantificada é o que torna a aplicação de um unificador mais geral uma regra sólida: uma vez que $\gamma (x')$ quer dizer que $\gamma$ é verdade para todo valor de $x'$,então $\gamma (t)$ é verdade para o termo $t$ que o unificador mais geral substitui $x$.
• Variáveis livres em um tableau são rígidas: todas as ocorrências da mesma variável têm de ser substituídas com o mesmo termo. Cada variável pode ser considerada um símbolo que representa um termo que ainda está para ser decidido. Isto é uma consequência das variáveis livres sendo assumido universalmente quantificada ao longo de toda a fórmula representada pelo quadro: se a mesma variável ocorre livre em dois nós diferentes, ambas as ocorrências estão no âmbito do mesmo quantificador. Como um exemplo, se as fórmulas em dois nós são $A(x)$ e $B(x)$, onde $x$ é livre em ambos, a fórmula representada pelo tableau é algo na forma $\forall x.(...A(x)...B(x)...)$. Esta fórmula implica que $(...A(x)...B(x)...)$ é verdade para qualquer valor de $x$, mas não implicam, em geral, $(...A(t)...A(t')...)$ para dois termos diferentes $t$ e $t'$, $x$ não pode ser substituído por dois termos diferentes de$A(x)$ e $B(x)$.
• Variáveis livres em uma fórmula para verificar a validade também são considerados universalmente quantificada. No entanto, essas variáveis não podem ser deixadas livres na construção de um tableau, porque as regras de tableau trabalham na conversão da fórmula, mas ainda tratam variáveis livres como universalmente quantificadas. Por exemplo, $P(x)\rightarrow P(c)$ não é válido (não é verdade no modelo, onde$D=\{1,2\},P(1)=\bot ,P(2)=\top ,c=1$, e a interpretação onde $x=2$). Consequentimente, $\{P(x),\neg P(c)\}$é satisfeita (que é satisfeita por o mesmo modelo e interpretação). No entanto, um tableau fechado poderia ser gerado com $P(x)$ e $\neg P(c)$, e substituindo $x$ por $c$ geraria um fechado. Um procedimento correto é primeiro fazer quantificadores universais explícito, gerando, assim,$\forall x.(P(x)\rightarrow P(c))$.

As seguintes duas variantes também são corretas.

• Aplicando-se a todo o tableau uma substituição às variáveis livres do tableau é uma regra correta, desde que essa substituição é livre para a fórmula que representa o tableau. Em outros mundos, aplicando-se tal substituição leva a um tableau cuja fórmula é ainda uma consequência do conjunto de entrada. Usando unificadores mais geral garantindo automaticamente que a condição de liberdade para o tableau é atendida.
• Embora, em geral, cada variável tem de ser substituída, com o mesmo termo, em todo o tableau, há alguns casos especiais em que não é necessário.

Tableaux com unificação pode ser provado como completo: se um conjunto de fórmulas é insatisfatível, ele tem um tableau com a unificação da prova. No entanto, na verdade, encontrar tal prova pode ser um problema difícil. Ao contrário do caso, sem unificação, a aplicação de uma substituição podem modificar a parte existente de um tableau; enquanto que a aplicação de uma substituição fecha, pelo menos, um ramo, ele pode fazer outros ramos impossível para fechar (mesmo se o conjunto é insatisfatível).

Uma solução para este problema é o atraso de instanciação: nenhuma substituição é aplicada até fechar todos os ramos, ao mesmo tempo que é encontrado. Com esta variante, uma prova para um insatisfatível pode sempre ser encontrada através de uma política adequada de aplicação das outras regras. Esse método, porém, exige que todo o tableau seja guardado na memória: o método geral fecha ramos, o que pode ser, então, descartado, enquanto esta variante não fechar qualquer ramo até o fim.

O problema é que alguns tableaux que podem ser gerados é impossível fechar, a menos se o conjunto é insatisfatível é comum a outros conjuntos de regras de expansão do tableau: mesmo se algumas sequências específicas de aplicação dessas regras permitem a construção de um tableau fechado (se o conjunto é insatisfatível), algumas outras sequências conduzem a tableaux que não podem ser fechados. Soluções gerais para estes casos são descritos na seção "Procurando um tableau fechado".

O cálculo de Tableau e suas propriedades

Um cálculo de tableau é um conjunto de regras que permite a construção e modificação de um tableau. Regras do tabelau proposicional, regras de tableau sem unificação, e regras de tableau com unificação, são todos cálculos de tableau. Algumas propriedades importantes de um cálculo de tableau podem ou não podem possuir são a integridade, destrutividade, e a prova de confluência.

Um cálculo de tableau é completo se ele permite a construção de um tableau de prova para cada dado conjunto insatisfatível de fórmulas. Os cálculos de tableau mencionados acima pode ser provados como completos.

Uma diferença notável entre o tableau com unificação e os outros dois cálculos é que os dois últimos cálculos apenas modificam um tableau pela adição de novos nós para ele, enquanto o outro faz substituições para modificar a parte existente do tableau. Mais geralmente, os cálculos de tableau são classificados como destrutivos ou não destrutivos , dependendo se eles apenas adicionam novos nós tableau ou não. O Tableau com unificação é, portanto, destrutivo, enquanto o proposicional e o sem unificação não são destrutivos.

Prova de confluência é a propriedade de um cálculo de tableau para obter uma prova para um conjunto insatisfatível arbitrário de um tableau arbitrário, supondo-se que, neste tableau, tem-se obtido aplicando-se as regras de cálculo. Em outras palavras, em uma prova confluente de cálculo de tableau, a partir de uma conjunto insatisfatível pode-se aplicar qualquer conjunto de regras e ainda obter um tableau a partir do qual um sistema fechado pode ser obtido através da aplicação de algumas outras regras.

Procedimentos de prova

Um cálculo de tableau é simplesmente um conjunto de regras que informa como um tableau pode ser modificado. Um procedimento de prova é um método para realmente encontrar uma prova (se existir). Em outras palavras, um cálculo de tableau é um conjunto de regras, enquanto que uma prova de procedimento é uma política de aplicação destas regras. Mesmo se um cálculo estiver completo, não a cada escolha possível de aplicação de regras conduz a uma prova de um conjunto insatisfatível. Por exemplo $\{P(f(x)),R(c),\neg P(f(c))\vee \neg R(c),\forall x.Q(x)\}$é insatisfatível, mas ambos os tableaux com unificação e tableaux sem unificação permitem a regra para os quantificadores universais ser aplicado repetidamente para a última fórmula, enquanto simplesmente aplicar a regra de disjunção para a terceira levaria diretamente para o fechamento.

Para o procedimento de prova, a definição de integralidade tem sido dada: um procedimento de prova é fortemente completo se permite encontrar um tableau fechado para qualquer conjunto insatisfatível de fórmulas. Prova de confluência a base de cálculo é relevante para a integralidade: prova de confluência é a garantia de que um tableau fechado pode ser sempre gerado a partir de um tableau arbitrário parcialmente construído (se o conjunto é insatisfatível). Sem a prova de confluência, a aplicação de um regra "errada" pode resultar na impossibilidade de fazer o tableau completo pela aplicação de outras regras.

O tableaux Proposicional e sem unificação possuem procedimentos de provas fortemente completos. Em particular, um procedimento de prova completo é o procedimento que aplicar as regras em um caminho justo. Isto é porque a única maneira que tais cálculos não permitem gerar um tableau fechado a partir de um insatisfatível é por não aplicar algumas das regras aplicáveis.

Para tableaux proposicional, quantidades equivalentes para a expansão de cada fórmula em cada ramo. Mais precisamente, para cada fórmula e cada ramo a fórmula é a regra de que a fórmula como uma pré-condição tem sido utilizada para expandir a ramificação. Um procedimento justo de prova para o tableaux proposicional é fortemente completo.

Para o tableaux de primeira ordem, sem unificação, a condição de equidade é semelhante, com a exceção que a regra do quantificador universal pode exigir mais do que uma aplicação. As quantidades equivalentes para se expandir a cada quantificador universal um número infinito de vezes. Em outras palavras, com uma política justa de aplicação das regras não é possível manter a aplicação de outras regras, sem se expandir a cada quantificador universal em todo ramo que ainda está aberto de vez em quando.

Procurando por um tableau fechado

Se um cálculo de tableau estiver concluído, cada conjunto insatisfatível de fórmulas tem associado um tableau fechado. Enquanto esse tableau pode sempre ser obtido através da aplicação de algumas das regras de cálculo, o problema de quais as regras aplicar para uma determinada fórmula ainda permanece. Como resultado, a integralidade não implica automaticamente a existência de uma política viável de aplicação de regras que sempre leva a um tableau fechado para cada dado conjunto insatísfativel de fórmulas. Enquanto uma prova justa de conclusão do processo para o tableau básico e tableau sem unificação, este não é o caso do tableau com unificação.

Uma solução geral para este problema é a de pesquisar o espaço do tableaux até um fechado ser encontrado (se algum existe, isto é, o conjunto é insatisfatível). Nesta abordagem, começa-se com um tableau vazio e, em seguida, recursivamente aplica-se todas as possíveis regras aplicáveis. Este procedimento visita uma árvore (implícita) cujos nós são rotulados com tableaux, e de tal forma que o tableau em um nó é obtido a partir do tableau em seu pai pela aplicação de uma das normas em vigor.

Uma vez que cada ramo pode ser infinito, esta árvore tem que ser visitada primeiro em largura, em vez de profundidade. Isso requer uma grande quantidade de espaços, como a largura da árvore pode crescer exponencialmente. Um método que pode visitar alguns dos nós mais do que uma vez, mas funciona no espaço polinômial é para se visitar em uma maneira depth-first comaprofundamento iterativo: uma primeira visita a árvore até uma certa profundidade, em seguida, aumenta a profundidade e realizar a visita novamente. Este procedimento utiliza a profundidade (que é também o número das regras de tableau que foram aplicadas) para decidir quando parar a cada passo. Vários outros parâmetros (tais como o tamanho do tableau de rotulagem de um nó) tem sido usado em vez disso.

A redução de busca

O tamanho da árvore de busca depende do número de tableau (filhos) que pode ser gerado a partir de um dado (pai). A redução do número de tal tableau, portanto, reduz a necessária pesquisa.

Um caminho para reduzir esse número é para não permitir a geração de alguns tableau com base em sua estrutura interna. Um exemplo é a condição de regularidade: se um ramo contém um literal, usando uma regra de expansão que gera o mesmo literal é inútil, porque o ramo que contém duas cópias dos literais teria o mesmo conjunto de fórmulas da original. Esta expansão pode ser anulada porque se um tableau fechado existe, pode ser encontrado sem ele. Esta restrição é estrutural porque pode ser verificado observando a estrutura do tableau para expandir.

Diferentes métodos para reduzir a pesquisa não permitem a geração de alguns tableau pelo fato de um tableau fechado ainda poder ser encontrado, expandindo os outros. Estas restrições são chamadas globais. Como um exemplo de uma restrição global, pode empregar-se uma regra que especifique qual dos ramos abertos é para ser expandido. Como resultado, se um tableau, por exemplo, tem dois ramos não-fechados, a regra diz que um é para ser expandido, não permitindo a expansão do segundo. Essa restrição reduz o espaço de busca, porque uma escolha possível agora é proibida; completamente se, contudo, não prejudicado, como o segundo ramo ainda será ampliado se o primeiro é finalmente fechado. Como um exemplo, um quadro com raiz $\neg a\wedge \neg b$, filho $a\vee b$, e duas folhas $a$ e $b$ podem ser fechados de duas maneiras: aplicando $(\wedge )$ primeiro para $a$ e depois para $b$, ou vice-versa. Claramente não há necessidade de seguir as duas possibilidades; pode-se considerar apenas o caso em que $(\wedge )$ é primeiro aplicado para $a$ e ignorar o caso em que é aplicado pela primeira vez a $b$. Esta é uma restrição global porque o que permite negligenciar esta segunda expansão é a presença do outro quadro, em que a expansão é aplicada a $a$ primeiro e depois $b$.

Cláusulas dos tableaux

Quando aplicado a um conjuntos de cláusulas (ao invés de fórmulas arbitrárias), o método de tableaux permite um certo número de melhorias de eficiência. Uma cláusula de primeira ordem é uma fórmula $\forall x_{1},\ldots ,x_{n}L_{1}\vee \cdots \vee L_{m}$ que não contém variáveis livres e de tal forma que cada $L_{i}$ é um literal. Os quantificadores universais são muitas vezes omitidos para maior clareza, de modo que, por exemplo, $P(x,y)\vee Q(f(x))$ significa, na verdade, $\forall x,y.P(x,y)\vee Q(f(x))$. Observe que, se tomadas literalmente, essas duas fórmulas não são as mesmas para satisfatibilidade: em vez disso, a satisfatibilidade de $P(x,y)\vee Q(f(x))$ é o mesmo que o de $\exists x,y.P(x,y)\vee Q(f(x))$. Que variáveis livres são universalmente quantificadas não é uma consequência da definição da satisfatibilidade na primeira ordem; é bastante utilizada como implícita uma suposição comum quando se lida com cláusulas.

As únicas regras de expansão que são aplicáveis a uma cláusula são $(\forall )$ e $(\vee )$; estas duas regras, pode ser substituído pela sua combinação, sem perder a integridade. Em particular, a regra a seguir corresponde a aplicar na sequência de regras $(\forall )$ e $(\vee )$ da primeira ordem de cálculo com unificação.

$(C){\frac {L_{1}\vee \cdots \vee L_{n}}{L_{1}'|\cdots |L_{n}'}}$ onde $L_{1}'\vee \cdots \vee L_{n}'$ é obtido através da substituição de cada variável com um novo $L_{1}\vee \cdots \vee L_{n}$

Quando o conjunto a ser verificado para satisfatibilidade é apenas composto de cláusulas, essa e as regras de unificação são suficientes para provar a insatisfatibilidade. Em outros mundos, o cálculos de tableaux que são compostos de $(C)$ e $(\sigma )$ é completo.

Desde que a regra de expansão de cláusula gere apenas literais e nunca cláusulas novas, as cláusulas a que pode ser aplicada apenas são cláusulas do conjunto de entrada. Como resultado, a regra de expansão de cláusula pode ser ainda mais restrito, para o caso em que a cláusula esta no conjunto de entrada.

$(C){\frac {L_{1}\vee \cdots \vee L_{n}}{L_{1}'|\cdots |L_{n}'}}$ onde $L_{1}'\vee \cdots \vee L_{n}'$ é obtido através da substituição de cada variável com um novo nó $L_{1}\vee \cdots \vee L_{n}$, que é uma cláusula do conjunto de entrada

Desde que esta regra explore diretamente as cláusulas em que o conjunto de entrada não é necessário para inicializar o tableau para a cadeia de cláusulas da entrada. O tableau inicial, portanto, pode ser inicializado com o único nó rotulado $true$; este rótulo é geralmente omitido como implícito. Como resultado desta simplificação, cada nó do tableau (exceto a raiz) é rotulada com um literal.

Uma série de otimizações podem ser utilizadas para a cláusula do tableau. Estas otimização são destinadas a reduzir o número de possíveis tableaux a ser explorado quando procurar um tableau fechado, conforme descrito na seção "Procurando por um tableau fechado" acima.

Tableau de conexão 

Conexão é uma condição sobre o tableau, que proíbe a expansão de um ramo, utilizando as cláusulas que não tenham relação com o literais que já estão no ramo. A conexão pode ser definida de duas maneiras:

conectividade forte

quando expandir um ramo, use uma cláusula da entrada somente se ele contém um literal que pode ser unificado com a negação do literal na folha atual

conectividade fraca

permitir a utilização de cláusulas que contêm um literal que unifica com a negação de um literal no ramo

Ambas as condições aplicam-se apenas aos ramos que consistem não apenas da raiz. A segunda definição permite a utilização de uma cláusula que preveja um literal que unifica com a negação de um literal no ramo, enquanto que o primeiro, a única restrição adicional, que o literal seja folha do ramo atual.

Se a cláusula de expansão é restrito por conectividade (forte ou fraca), a sua aplicação produz um tableau em que a substituição pode se aplicada a uma das folhas novas, fechando seu ramo. Em particular, esta é a folha que contém o literal da cláusula que unifica com a negação de um literal no ramo (ou a negação do literal no pai, no caso de uma conexão forte).

Ambas as condições de conectividade conduz a um cálculo de primeira ordem: se um conjunto de cláusulas é insatisfatível, ele tem uma tableau de conexão fechado (fortemente ou fracamente) . Como um tableau fechado pode ser encontrada através de pesquisa no espaço de tableaux, como explicado na seção "Procurando por um tableau fechado". Durante essa busca, a conectividade elimina algumas possíveis escolhas de expansão, reduzindo, assim, a procura. Em outros mundos, enquanto o tableau em um nó da árvore pode ser em geral expandido de várias formas diferentes, a conexão pode permitir apenas alguns deles, reduzindo assim o número de resultados do tableaux que precisa ser ampliado ainda mais.

Isso pode ser visto no seguinte exemplo (proposicional). O tableau feito de uma cadeia $true-a$ para o conjunto de cláusulas $\{a,\neg a\vee b,\neg c\vee d,\neg b\}$ pode ser em geral expandida usando cada um das quatro cláusulas da entrada, mas a ligação só permite a expansão que usa $\neg a\vee b$. Isto significa que a árvore de tableaux tem quatro folhas em geral, mas apenas se a conectividade é imposta. Isso significa que a conectividade deixa apenas um tableau para tentar expandir, em vez dos quatro únicos a considerar em geral. Apesar desta redução de escolhas, oteorema da completude implica que um tableau fechado pode ser encontrado se o conjunto é insatisfatível.

As condições de conectividade, quando aplicadas ao caso proposicional (clausal), faz a resultante do cálculo não-confluente. Como por exemplo, $\{a,b,\neg b\}$ é insatisfatível, mas a aplicação de $(C)$ para $a$ gera a cadeia de $true-a$, que não está fechado e que nenhuma outra regra de expansão pode ser aplicada sem violar a conectividade forte ou fraca. No caso de conexão fraca, a confluência detém, desde que a cláusula usada para expandir a raiz é relevante para a insatisfatibilidade, isso é, ele está contido em um subconjunto minimamente insatisfativel de um conjunto de cláusulas. Infelizmente, o problema de verificar se uma cláusula satisfaz esta condição é em si um problema difícil. Apesar da não-confluência, um tableau fechado pode ser encontrado através de uma pesquisa, como apresentado na seção acima "Procurando por um tableau fechado". Enquanto a pesquisa é necessária, a conectividade reduz as opções possíveis de expansão, tornando a pesquisa mais eficiente.

Tableaux regulares 

Um tableau é regular se nenhum literal ocorre duas vezes no mesmo ramo. Impor essa condição permite uma redução das possíveis escolhas do tableau de expansão, como as cláusulas que iriam gerar uma tableau não-regular não podem ser expandidas.

Estas etapas proibidas de expansão são, porém, inúteis. Se $B$ é um ramo que contém um literal $L$ e $C$ é uma cláusula cuja expansão viola a regularidade, então, $C$ contém $L$. Para fechar o tableau, o necessário para expandir e fechar, entre outros, o ramo onde $B-L$, onde $L$ ocorre duas vezes. No entanto, as fórmulas deste ramo são exatamente as mesmas que as fórmulas de $B$ sozinhas. Como resultado, os mesmos passos de expansão que fecham $B-L$ também fecham $B$. Isso significa que a expansão $C$ era desnecessária; além disso, se $C$ continha outros literais, sua expansão geraria outras folhas que precisariam ser fechadas. No caso proposicional, a expansão necessária para fechar estas folhas são completamente inúteis; no caso da lógica de primeira ordem, eles só podem afetar o resto do tableau, porque algumas unificações, podem, contudo, ser combinadas para as substituições usadas para fechar o resto do tableau.

Tableaux para a lógica modal

Em lógica modal, um modelo composto por um conjunto de mundos possíveis, cada um deles associado a uma valoração verdade; uma relação de acessibilidade indica quando um mundo é acessível a partir de outro. Um formula modal pode especificar não apenas condições sobre um mundo possível, mas também sobre aqueles que são acessíveis a partir do mesmo. Como por exemplo, $\Box A$ é verdadeira em um mundo que se $A$ é verdadeira em todos os mundos acessíveis a partir do mesmo.

Como para a lógica proposicional, os tableaux para a lógica modal são baseados em recursivamente quebrar fórmulas em seus componentes básicos. A expansão de um fórmula modal pode, no entanto, exigir condições sobre mundos diferentes. Como exemplo, se $\neg \Box A$ é verdade num mundo em que existe um mundo acessível a partir de onde $A$ é falso. No entanto, não se pode simplesmente adicionar a seguinte regra para a lógica proposicional.

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

No tableaux proposicional todas as fórmulas que se referem a mesma valoração verdade, mas a pré-condição da regra anterior mantém em um mundo ao mesmo tempo, em consequência detém no outro. Não levando em conta isso iria gerar resultados errados. Por exemplo, a fórmula $a\wedge \neg \Box a$ os estados que $a$ é verdade no mundo atual e $a$ é falso em um mundo que é acessível a partir do mesmo. A simples aplicação de $(\wedge )$ e a regra de expansão  acima produziria $a$ e $\neg a$, mas estas duas fórmulas não deve, em geral, produzir uma contradição, como eles têm mundos diferentes. Os cálculos de tableaux modal contêm regras do tipo da anterior, mas incluiem mecanismos para evitar a interação incorreta de fórmulas, referindo-se a mundos diferentes.

Tecnicamente, os tableaux para a lógica modal verificam a satisfatibilidade de um conjunto de fórmulas: eles verificam se existe um modelo de $M$ e do mundo $w$ de tal forma que as fórmulas do conjunto são verdadeiras, nesse modelo e mundo. No exemplo acima, enquanto $a$ afirma a verdade de $a$ no $w$, a fórmula $\neg \Box a$ afirma a verdade de $\neg a$ em alguma mundo $w'$ que é acessível a partir de $w$ e que pode, em geral, ser diferente de $w$. Cálculos de tableaux para a lógica modal levar em conta que as fórmulas podem referir-se a mundos diferentes.

Este fato tem uma consequência importante: fórmulas que têm um mundo podem implicar condições sobre diferentes sucessores daquele mundo. A insatisfatibilidade pode então ser provada a partir do subconjunto de fórmulas referentes a um único sucessor. Isto é, se um mundo pode ter mais de um sucessor, o que é verdade para a lógica modal. Se este for o caso, uma fórmula como  $\neg \Box A\wedge \neg \Box B$ é verdadeira se um sucessor, onde $\neg A$ detém e existe, e um sucessor, onde $\neg B$ detém e existe. No contrário, se pode mostrar a insatisfatibilidade de $\neg A$ em um successor arbitrário, a fórmula é provada insatisfatível sem verificar se há mundos onde $\neg B$ se mantem. Ao mesmo tempo, se se pode mostrar a insatisfatibilidade de $\neg B$, não há necessidade de checar a $\neg A$. Como resultado, se há dois mundos para expandir $\neg \Box A\wedge \neg \Box B$, uma destas duas maneiras é sempre suficiente para provar a insatisfatibilidade se a fórmula for insatisfatível. Por exemplo, pode-se expandir o tableau, considerando um mundo arbitrário, onde $\neg A$ mantém. $\neg B$ se $\neg \Box A$ apenas, ou $\neg \Box B$ apenas; No entanto, se a escolha errada é feita, o tableau resultante pode não ser fechado. Expandindo ambas as subfórmulas levam a cálculos de tableau que são completos, mas não à provas de confluentes. Pesquisando conforme descrito no "Procurando por um tableau fechado" pode, portanto, ser necessário.

Dependendo se a pré-condição e consequência de uma regra de expansão de tableau, referem-se ao mesmo mundo ou não, a regra é chamada de estática ou transacional. Enquanto as regras de conectivos proposicionais são todas estáticas, nem todas as regras para os conectivos modais são transacionais: por exemplo, em cada lógica modal, incluindo o axioma de T, ele tem que $\Box A$ implica $A$ no mesmo mundo. Como resultado, o tableau relativo (modal) da regra de expansão é estático, como sua pré-condição e consequência referem-se ao mesmo mundo.

Tableau fórmula-exclusão

Uma maneira para fazer fórmulas, referindo-se a mundos diferentes, não interagindo no caminho errado, é para certificar-se de que todas as fórmulas de um ramo referem-se ao mesmo mundo. Esta condição é inicialmente verdade, como todas as fórmulas em um conjunto para ser verificada a consistência são consideradas referências para o mesmo mundo. Quando expandir uma ramificação, duas situações são possíveis: ou a fórmulas novas referem-se ao mesmo mundo, como outro no ramo, ou não. No primeiro caso, a regra é aplicada normalmente. No segundo caso, todas as fórmulas do ramo que também não mantém o novo mundo, são excluídos do ramo, e possivelmente adicionados para todos os outros ramos que estão ainda em relação ao velho mundo.

Como por exemplo, em S5 cada fórmula $\Box A$ é verdade em um mundo, também é verdade em todos os mundos acessíveis (isto é, em todos os mundos acessíveis tanto $A$ e $\Box A$ são verdadeiros). Portanto, ao aplicar ${\frac {\neg \Box A}{\neg A}}$ cuja consequência possui em um mundo diferente, um exclui todas as fórmulas do ramo, mas pode manter todas as fórmulas $\Box A$, pois estas têm no novo mundo. A fim de manter a integridade, as fórmulas deletadas são então adicionadas para todos os outros ramos que ainda se referem ao velho mundo.

Tableau mundo-marcado 

Um mecanismo diferente para garantir a correta interação entre fórmulas referindo-se a mundos diferentes, é mudar a partir de fórmulas para fórmulas marcadas: em vez de escrever $A$ escrever $w:A$ para torná-lo explícito que $A$ possui no mundo $w$.

Todas as regras de expansão proposicional são adaptadas para esta variante, afirmando que todos eles se referem a fórmulas com a mesma etiqueta. Por exemplo, $w:A\wedge B$ gera dois nós rotulados com $w:A$ e $w:B$; um ramo é fechado apenas se contém dois opostos literais do mesmo mundo, como $w:a$ e $w:\neg a$; o encerramento não é gerado se os dois macadores são diferentes, como em $w:a$ e $w':\neg a$.

A regra de expansão modal pode ter uma consequências que se referem a mundos diferentes. Por exemplo, a regra para $\neg \Box A$ poderia ser escrito da seguinte forma

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

A pré-condição e a consequente desta regra se referem aos mundos $w$ e $w'$, respectivamente. Os vários cálculos utilizam métodos diferentes para controlar a acessibilidade dos mundos usados como marcados. Alguns incluem pseudo-fórmulas como $wRw'$ para indicar que $w'$ é acessível a partir de $w$. Outros usam sequências de números inteiros, como mundo de marcações, esta notação representa, implicitamente, a relação de acessibilidade (por exemplo, $(1,4,2,3)$ é acessível a partir de $(1,4,2)$.)

Tableaux de conjuntos-marcados 

O problema da interação entre fórmulas mantidas em mundos diferentes podem ser superadas utilizando o tableaux de conjuntos marcados. Estas são árvores cujos nós são marcados com conjuntos de fórmulas; as regras de expansão dizem como anexar novos nós de uma folha, com base apenas na marcação da folha (e não no rótulo dos outros nós no ramo).

O tableaux para a lógica modal é utilizado para verificar a satisfatibilidade de um conjunto de fórmulas modais em uma dada lógica modal. Dado um conjunto de fórmulas ${\displaystyle }$$S$, ele verifica a existência de um modelo de $M$ e um mundo $w$ de tal forma que $M,w\models S$.

As regras de expansão dependem da lógica modal utilizada. Um sistema de tableau básico de lógica modal K pode ser obtido adicionando-se ao tableau proposicional as regras a seguir:

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

Intuitivamente, a pré-condição para esta regra expressar a verdade de todas as fórmulas $A_{1},\ldots ,A_{n}$ em todos os mundos acessíveis, e a verdade do $\neg B$ em alguns mundos acessível. A conseqüência dessa regra é uma fórmula que deve ser verdadeira em um desses mundos onde $\neg B$ é verdade.

Mais tecnicamente, os métodos de tableaux modais verificam a existência de um modelo de $M$ e um mundo $w$ que fazem o conjunto de fórmulas verdadeiro. Se $\Box A_{1};\ldots ;\Box A_{n};\neg \Box B$ são verdadeiros no $w$, deve haver um mundo $w'$ que é acessível a partir de $w$ e que faz $A_{1};\ldots ;A_{n};\neg B$ verdade. Esta regra, portanto, equivale a derivação de um conjunto de fórmulas que devem ser satisfeitas em tal $w'$.

Enquanto as pré-condições $\Box A_{1};\ldots ;\Box A_{n};\neg \Box B$ presume-se satisfeito por $M$, $w$ consequências $A_{1};\ldots ;A_{n};\neg B$ presume-se satisfeito em $M,w'$: o mesmo modelo, mas, possivelmente, diferentes mundos. O tableaux de conjunto-marcado não explicitamente mantem o controle do mundo, onde cada fórmula é assumida como verdadeira: dois nós podem ou não se referir ao mesmo mundo. No entanto, as fórmulas de marcação de um determinado nó são assumidas como verdadeiras, no mesmo mundo.

Como resultado da possibilidade de diferentes mundos onde fórmulas são assumidas como verdadeiras, uma fórmula em um nó não é automaticamente válida em todos os seus descendentes, como a aplicação da regra modal, correspondem a uma mudança de um mundo para outro. Esta condição é automaticamente capturada pelo tableaux de conjunto-marcado, como as regras de expansão são baseadas apenas nas folhas, onde são aplicadas e não sobre os seus antepassados.

Notavelmente, $(K)$ não estende diretamente para múltiplas fórmulas negadas encapsuladas, tais como em $\Box A_{1};\ldots ;\Box A_{n};\neg \Box B_{1};\neg \Box B_{2}$: enquanto existe um mundo acessível onde $B_{1}$ é falso, e no qual $B_{2}$ é falso, esses dois mundos não são necessariamente os mesmos.

Diferentemente das regras proposicionais, $(K)$ condições de estados sobre todas as suas pré-condições. Por exemplo, ele não pode ser aplicada a um nó marcado por $a;\Box b;\Box (b\rightarrow c);\neg \Box c$; enquanto este conjunto é inconsistente e isso pode ser facilmente comprovado através da aplicação $(K)$, essa regra não pode ser aplicada devido a fórmula $a$, que nem é relevante para a inconsistência. A remoção de tais fórmulas é possível pela regra:

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

A adição desta regra (regra de afinamento) faz com que a resultante do cálculo não-confluente: um tableau para um conjunto inconsistente pode ser impossível para fechar, mesmo se um tableau fechado para o mesmo conjunto existe.

A regra $(\theta )$ é não-determinística: o conjunto de fórmulas a ser removido (ou para ser mantido) pode ser escolhido arbitrariamente; isto cria o problema da escolha de um conjunto de fórmulas para descartar o que não é tão grande que faz com que o conjunto resultante pode ser satisfeito e não tão pequena que faz a necessária da aplicação de regras de expansão. Ter um grande número de possíveis escolhas faz com que o problema de procurar um tableau fechado se torne ainda mais difícil.

Este não-determinismo pode ser evitado por restringir o uso de $(\theta )$ de modo que só é aplicada antes de um regra de expansão modal, e para que ele apenas remove as fórmulas que fazem com que outra regra seja aplicável. Esta condição também pode ser formulada através da fusão de duas regras em uma única. A regra resultante produz o mesmo resultado que o antigo, mas implicitamente descarta todas as fórmulas que fez a velha regra não aplicável. Este mecanismo para a remoção de $(\theta )$ tem sido provado para preservar a integridade de muitas lógicas modais.

O axioma T expressa a reflexividade da relação de acessibilidade: todo mundo é acessível a partir de si mesmo. O correspondente da regra de expansão do tableau é:

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

Esta regra diz respeito a condições sobre o mesmo mundo: se $\Box B$ é verdadeira em um mundo, pela reflexividade $B$ é também verdadeiro no mesmo mundo. Esta regra é estática, não transacional, como sua pré-condição e a consequente referem-se ao mesmo mundo.

Esta regra copia $\Box B$ desde a pré-condição para a consequente, apesar de esta fórmula ter sido "usada" para gerar $B$. Isso é correto, como mundo considerado é o mesmo, então $\Box B$ também tem lá. Esta "cópia" é necessária, em alguns casos. Ele é, por exemplo, necessário para provar a inconsistência do $\Box (a\wedge \neg \Box a)$: as únicas regras aplicáveis são, em ordem, $(T),(\wedge ),(\theta ),(K)$, a partir do qual uma está bloqueada, se $\Box a$ não é copiada.

Tableaux auxiliares

Um método diferente para lidar com fórmulas mantidas em mundos alternativos para iniciar um tableau diferente para cada novo mundo que é introduzido no tableau. Por exemplo, $\neg \Box A$ implica que $A$ é falso no mundo acessível, então, se inicia uma novo tableau enraizado $\neg A$. Este novo tableau é anexado para o nó original do tableau onde a regra de expansão tem sido aplicada; o fechamento deste tableau gera imediatamente o fechamento de todos os ramos onde esse nó esta, independentemente, de o mesmo nó esta associado a outros tableaux auxiliares. As regras de expansão para tableaux auxiliares são as mesmas que o original; portanto, um tableau auxiliar pode ter, em outros turnos, tableaux (sub)auxiliares.

Pressupostos globais

O tableaux modal acima estabelece a consistência de um conjunto de fórmulas, e pode ser usado para solucionar o problema da consequência lógica local. Esse é o problema de dizer se, para cada modelo $M$, se $A$ é verdadeira em um mundo $w$, então $B$ é também verdadeiro no mesmo mundo. Isso é o mesmo que verificar se $B$ é verdadeiro em um mundo de um modelo, na suposição de que $A$ é também verdadeiro no mesmo mundo do mesmo modelo.

Um problema relacionado é o problema da consequência global, onde o pressuposto é que uma fórmula (ou conjunto de fórmulas) $G$ é verdadeira em todos os mundos possíveis do modelo. O problema é que verificar, se em todos os modelos $M$ onde $G$ é verdadeira em todos os mundos, $B$ também é verdadeiro em todos os mundos.

Os pressupostos locais e os globais em diferentes modelos onde a suposta fórmula é verdadeira em alguns mundos, mas não em outros. Como por exemplo, $\{P,\neg \Box (P\wedge Q)\}$ implica $\neg \Box Q$ globalmente, mas não localmente. A consequência local não possui um modelo constituido de dois mundos, fazendo $P$ e $\neg P,Q$ verdadeiro, respectivamente, e que o segundo é acessível a partir do primeiro; no primeiro mundo, a suposição é verdadeira, mas $\Box Q$ é falso. Este contra-exemplo funciona porque $P$ pode ser assumido como verdadeiro em um mundo e falso no outro. Se, porém, a mesma suposição é considerada global, $\neg P$ não é permitido em qualquer mundo do modelo.

Estes dois problemas podem ser combinados, de modo que se pode verificar se $B$ é uma consequência local de $A$ assumido no âmbito global $G$. Os cálculos de tableaux podem lidar com o pressuposto global por uma regra, permitindo a sua adição para cada nó, independentemente, do mundo que ele se refere.

Notações

As seguintes convenções são usadas às vezes.

Notação uniforme

Ao escrever regras de expansão de tableaux, fórmulas são frequentemente notadas usando uma convenção, de modo que, por exemplo, $\alpha$ é sempre considerado para ser $\alpha _{1}\wedge \alpha _{2}$. A tabela a seguir fornece a notação para as fórmulas proposicionais, de primeira ordem e lógica modal.

Notação	Formula
$\alpha$	$\alpha _{1}\wedge \alpha _{2}$	$\neg ({\overline {\alpha _{1}}}\vee {\overline {\alpha _{2}}})$	$\neg (\alpha _{1}\rightarrow {\overline {\alpha _{2}}})$
$\beta$	$\beta _{1}\vee \beta _{2}$	${\overline {\beta _{1}}}\rightarrow \beta _{2}$	$\neg ({\overline {\beta _{1}}}\wedge {\overline {\beta _{2}}})$
$\gamma$	$\forall x\gamma _{1}(x)$	$\neg \exists x{\overline {\gamma _{1}(x)}}$
$\delta$	$\exists x\delta _{1}(x)$	$\neg \forall x{\overline {\delta _{1}(x)}}$
$\pi$	$\Diamond \pi _{1}$	$\neg \Box {\overline {\pi _{1}}}$
$\upsilon$	$\Box \upsilon _{1}$	$\neg \Diamond {\overline {\upsilon _{1}}}$

Cada notação na primeira coluna é levado a qualquer fórmula nas outras colunas. Um fórmula barrada, tal como ${\overline {\alpha _{1}}}$ indica que $\alpha _{1}$ é a negação de qualquer que seja a fórmula que aparece em seu lugar, de modo que, por exemplo, na fórmula $\neg (a\vee b)$ a subformula $\alpha _{1}$ é a negação da $a$.

Uma vez que cada etiqueta indica muitas fórmulas equivalentes, esta notação permite escrever uma única regra para todas estas fórmulas equivalentes. Por exemplo, o conjunto de regra de expansão é formulado como:

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

fórmulas assinadas

Uma fórmula em um tableau é assumida como verdadeira. Tableaux assinados permitem afirmar que uma fórmula é falsa. Isto é geralmente obtido através da adição de um marcado para cada fórmula, onde o marcador T indica fórmulas assumidas como verdadeiras e F aqueles supostamente falsas. Um diferente, mas equivalente a notação, é que para escrever fórmulas que são considerados verdadeiras à esquerda do nó e fórmulas assumidas como falsas em sua direita.

Veja também

• Resolução (lógica)

Referências

• Beth, Evert W., 1955. "Semantic entailment and formal derivability", Mededelingen van de Koninklijke Nederlandse Akademie van Wetenschappen, Afdeling Letterkunde, N. R. Vol 18, nº 13, de 1955, pp 309-42. Reimpresso em Jaakko Intikka (ed.) The Philosophy of Mathematics, Oxford University Press, 1969.
• Bostock, David, 1997. Intermediate Logic. Oxford Univ. Prima.
• M D Agostino, D Gabbay, R Haehnle, J Posegga (Eds), Handbook of Tableau Methods, Kluwer,1999.
• Girle, Haste, 2000. Modal Logics and Philosophy. Teddington Reino Unido: Acumen.
• Goré, Rajeev (1999) "Tableau Methods for Modal and Temporal Logics" em D'Agostino, M., Dov Gabbay, R. Haehnle, e J. Posegga, eds., Handbook of Tableau Methods. Kluwer: 297-396.
• Richard Jeffrey, 1990 (1967). Formal Logic: Its Scope and Limits, 3ª ed. McGraw Hill.
• Raymond Smullyan, 1995 (1968). First Order-Logic. Dover Publications.
• Melvin Montagem (1996). First-order logic and automated theorem proving (2ª ed.). Springer-Verlag.
• Reiner Hähnle (2001). Tableaux and Related Methods. Handbook of Automated Reasoning
• Reinhold Letz, Gernot Stenz (2001). Model Elimination and Connection Tableau Procedures. Handbook of Automated Reasoning
• Zeman, J. J. (1973) Lógica Modal. Reidel.

Ligações externas

• «TABLEAUX». : uma conferência internacional sobre raciocínio automatizado com tableaux analíticos e métodos relacionados. 
• «JAR». : Diário de Raciocínio Automatizado. 
• «lolo». : um teorema provador simples escrito em Haskell que usa tableaux analíticos para a lógica proposicional. 
• «Os tableaux pacote». : provador interativo para lógica proposicional e a lógica de primeira ordem usando tableaux. 
• «Árvore de prova gerador». : outro provador interativo para lógica proposicional e a lógica de primeira ordem usando tableaux. 
• «LoTREC». Um tableaux genérico baseado no provador para a lógica modal da universidade de IRIT/Toulouse.