Raciocínio por Tablôs de uma Forma Direta

Arthur Buchsbaum, Maurício Correia Lemes Neto
DOI: https://doi.org/10.21529/RESI.2005.0402001

Texto completo:

PDF

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

Palavras-chave

Tablô; Sistema de Tablôs; Método Direto; Método Indireto; Método da Refutação