Na teoria da prova, o tableau semântico (; 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 ideia 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 implicam em se é 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. miniaturadaimagem|120x120px|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 ; neste segundo caso, o procedimento pode sempre copiar uma fórmula no conjunto abaixo de uma folha. Como exemplo, o tableau para o conjunto é 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 miniaturadaimagem|260x260px|((a⋁¬b)⋀b) gera (a⋁¬b) e (b) Sempre que um ramo de um tableau contém uma fórmula 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: Se um ramo do tableau contém uma fórmula conjuntiva , adicionar a sua folha uma cadeia de dois nós que contém as fórmulas e Esta regra é geralmente escrita como segue:
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 no final de um ramo que contém . Mais precisamente, se um nó em um ramo é rotulado pode-se juntar ao ramo da nova folha .
Disjunção miniaturadaimagem|330x330px|(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 seguinte regra pode ser aplicada: Se um nó em um ramo contém uma fórmula disjuntiva , em seguida, cria-se dois filhos para a folha do ramo, contendo e , 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 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:
Se nós, presume-se que contenham um conjuntos de fórmulas, esta regra é substituída pelo seguinte: se um nó é rotulado , em uma folha do ramo, podem ser acrescentados dois nós filhos rotulados e , 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, é tratado como . Regras para introduzir ou remover um par de opostos (como em ) também são usados neste caso (caso contrário, não haveria nenhuma forma de expansão de uma fórmula como :
miniaturadaimagem|403x403px|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.) miniaturadaimagem|314x314px|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 com o conjunto que contém tanto e no lugar dele. Em particular, se uma folha é marcada com um nó pode ser acrescentado a ele com a marcação :
Para a disjunção, um conjunto é equivalente a disjunção de dois conjuntos e . Como resultado, se o primeiro conjunto marcado for uma folha, dois filhos podem ser acrescentados, marcado com as duas últimas fórmulas.
Finalmente, se um conjunto contém um literal e a sua negação, este ramo pode ser 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.