Raciocínio por Tablôs de uma Forma Direta

Resumo

Este artigo apresenta uma forma alternativa de geração de árvores de provas por tablôs. Denominamos esse método de direto, por causa de característica em que a possível conclusão é inserida no tablô inicial, sem negá-la. Já o método dos tablôs por refutação se utiliza da negação da possível conclusão. No sistema de tablôs por prova direta para a lógica clássica, cada ramo corresponde semanticamente à disjunção das fórmulas que o compõem, e cada tablô equivale semanticamente à conjunção de todas essas disjunções. Em qualquer um dos métodos baseados em tablôs para a Lógica Clássica, tanto direto quanto indireto, um ramo é considerado fechado se o mesmo contiver duas fórmulas contraditórias. No método direto o fechamento de um ramo acarreta a sua validade semântica, a qual por sua vez implica, no caso do fechamento de todos os ramos, na validade da possível conclusão. Já no método indireto o fechamento de todos os ramos acarreta a insatisfatibilidade da negação da possível conclusão, o que por sua vez implica na validade da mesma