Um método dos tablôs por prova direta para a lógica clássica
Show full item record
Title:
|
Um método dos tablôs por prova direta para a lógica clássica |
Author:
|
Lemes Neto, Maurício Correia
|
Abstract:
|
Este trabalho desenvolve uma forma diferente de se obter árvores de prova por tablôs. Denominamos esse método de direto, por causa da 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 está relacionado semanticamente à disjunção das fórmulas que o compõem, e o tablô completo corresponde 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 corresponde à sua validade semântica, a qual implica, no caso do fechamento de todos os ramos, na validade da possível conclusão. Já no método indireto o fechamento de um ramo corresponde à insatisfatibilidade da negação da possível conclusão, o que por sua vez implica na validade da mesma. |
Description:
|
Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico. Programa de Pós-Graduação em Ciência da Computação. |
URI:
|
http://repositorio.ufsc.br/xmlui/handle/123456789/87630
|
Date:
|
2004 |
Files in this item
This item appears in the following Collection(s)
Show full item record
Search DSpace
Browse
-
All of DSpace
-
This Collection
My Account
Statistics
Compartilhar