Made available in DSpace on 2014-06-12T16:01:20Z (GMT). No. of bitstreams: 2
arquivo7782_1.pdf: 981863 bytes, checksum: b65d9631609e56e387c6959338c69466 (MD5)
license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5)
Previous issue date: 2005 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / Os principais métodos da teoria da prova geral são: eliminação-do-corte e normalização.
Na teoria da prova há diversos trabalhos voltados ao teorema da eliminação-do-corte para
o cálculo de sequentes clássico, bem como, investigações direcionadas à normalização
para a dedução natural (DN) clássica. Por outro lado, são encontrados poucos trabalhos
que buscam definir a normalização para a lógica clássica, através de uma estrutura
de prova com mais de uma conclusão. Mencionem-se dois autores que apresentam
normalização para uma estrutura com mais de uma conclusão, e.g. Ungar [Ung92] e
Cellucci [Cel92]. Todavia, nenhuma investigação apresenta um tratamento direcionado
às questões inerentes à definição de um procedimento de normalização dentro de uma
estrutura de prova com mais de uma conclusão, onde as derivações sejam, de fato, representadas
como grafos-de-prova. Portanto, o objetivo central deste trabalho é a definição
do procedimento de normalização para os N-Grafos. Os N-Grafos foram definidos por de
Oliveira e compõem um sistema de provas simétrico para a DN, onde as regras lógicas
e estruturais são apresentadas em uma estrutura de prova com múltipla conclusão e as
derivações são representadas como dígrafos. Para a definição da normalização dos NGrafos,
foram construídos cinco conjuntos de reduções: lógicas, estruturais, com ciclos,
sequência com repetição de ciclos entrelaçados e permutação do enfraquecimento. Essas
reduções foram baseadas nos trabalhos de Prawitz, Ungar e Cellucci, bem como, inspiradas
pela própria estrutura de múltipla conclusão dos N-Grafos. Ademais, foram definidos
o teorema e a prova da normalização, sendo que a prova foi construída de forma direta,
diferentemente da prova indireta dada por Ungar. Posteriormente, foram estabelecidas
as propriedades da terminação e da confluência (fraca) para a normalização dos N-Grafos.
Através da construção da normalização para os N-Grafos é possível destacar algumas propostas
de trabalhos futuros como, por exemplo, a relação entre provas formais e processos
concorrentes, e a investigação da correspondência entre a normalização e a identidade de
provas
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufpe.br:123456789/2817 |
| Date | January 2005 |
| Creators | Vaz Alves, Gleifer |
| Contributors | José Guerra Barreto de Queiroz, Ruy |
| Publisher | Universidade Federal de Pernambuco |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Source | reponame:Repositório Institucional da UFPE, instname:Universidade Federal de Pernambuco, instacron:UFPE |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0104 seconds