Made available in DSpace on 2014-06-12T15:49:50Z (GMT). No. of bitstreams: 1
license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5)
Previous issue date: 2009 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / O presente trabalho é baseada em dois aspectos fundamentais: (i) o estudo de procedimentos
de normalização para sistemas de provas, especialmente para a lógica clássica com dedução
natural; e (ii) a investigação de técnicas da perspectiva geométrica aplicadas em propriedades
da teoria da prova. Com isso, a motivação específica deste trabalho reside principalmente na
análise daqueles trabalhos que estão voltados à definição de técnicas da normalização através
de mecanismos da perspectiva geométrica. Destaca-se que técnicas da perspectiva geométrica
trazem o uso de arcabouços gráficos e/ou topológicos com a finalidade de representar sistemas
formais de provas e suas propriedades. Dessa forma, a primeira parte do documento apresenta
o uso de técnicas e arcabouços topológicos para estabelecer algumas propriedades, como, por
exemplo, o critério de corretude e a normalização de sistemas de prova. Ao passo que a segunda
parte do documento é inicialmente direcionada à descrição de algumas abordagens de
normalização (principalmente) para a lógica clássica com dedução natural. E o complemento
da segunda parte é dedicado à definição do principal objetivo do trabalho, i.e., desenvolver um
procedimento de normalização para o conjunto completo de operadores dos N-Grafos, através
do auxílio de algumas técnicas de perspectiva geométrica. (Destaca-se que as técnicas de perspectiva
geométrica, aplicadas à normalização dos N-Grafos, não fazem uso de arcabouços
topológicos). N-Grafos é um sistema de prova com múltipla conclusão definido para lógica
clássica proposicional com dedução natural. Ademais, os N-Grafos possuem tanto regras lógicas
como estruturais, estruturas cíclicas são permitidas e além disso as derivações são representadas
como grafos direcionados. De fato, a princpal característica do procedimento de
normalização aqui apresentado é fornecer um tratamento completo para as estruturas cíclicas.
Ou seja, são definidas classes de ciclos válidos, critério de corretude, propriedades e ainda
um algoritmo específico para normalizar os ciclos nos N-Grafos. Destaca-se que esses elementos
são construídos através do auxílio de arcabouços gráficos. Além disso, o mecanismo
de normalização é capaz de lidar com os diferentes papéis executados pelos operadores ?/>.
Adicionalmente, apresenta-se uma prova direta da normalização fraca para os N-Grafos, bem
como, a determinação das propriedades da subfórmula e da separação
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufpe.br:123456789/1418 |
| Date | 31 January 2009 |
| Creators | Vaz Alves, Gleifer |
| Contributors | José Guerra Barreto de Queiroz, Ruy |
| Publisher | Universidade Federal de Pernambuco |
| Source Sets | IBICT Brazilian ETDs |
| Language | English |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/doctoralThesis |
| Source | reponame:Repositório Institucional da UFPE, instname:Universidade Federal de Pernambuco, instacron:UFPE |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0343 seconds