Submitted by Luiz Felipe Barbosa (luiz.fbabreu2@ufpe.br) on 2015-03-12T14:54:25Z
No. of bitstreams: 2
Dissertacao Ruan Carvalho.pdf: 760651 bytes, checksum: 11973d9d0a63868703fa87f2c9daf83b (MD5)
license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) / Approved for entry into archive by Daniella Sodre (daniella.sodre@ufpe.br) on 2015-03-13T13:14:37Z (GMT) No. of bitstreams: 2
Dissertacao Ruan Carvalho.pdf: 760651 bytes, checksum: 11973d9d0a63868703fa87f2c9daf83b (MD5)
license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) / Made available in DSpace on 2015-03-13T13:14:37Z (GMT). No. of bitstreams: 2
Dissertacao Ruan Carvalho.pdf: 760651 bytes, checksum: 11973d9d0a63868703fa87f2c9daf83b (MD5)
license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5)
Previous issue date: 2013-10-03 / Desde que proof-nets para MLL− foram introduzidas por Girard, vários estudos foram realizados
na prova de corretude desse sistema. O primeiro critério foi o no shorttrip condition: Girard
usou a noção de trips para definir impérios e provou que se todas as fórmulas terminais numa
proof-net R forem conclusões de links
ou de axiomas, então pelo menos um link terminal
divide R em duas partes (a conclusão deste link é chamada de “nó split”).
Outro avanço na prova de corretude de proof-nets foi obtido pela introdução de um novo tipo
de subnets. Uma vez que a noção de reinos foi introduzida, Bellin & van de Wiele produziram
uma elegante prova do teorema de sequentização utilizando propriedades simples das subnets e
mostrando como encontrar o nó split. Todavia, estas abordagens não se aplicam integralmente
aos N-Grafos, uma vez que a noção de reinos não é possível de ser empregada.
Não obstante, a necessidade de identificar o nó split está no coração da prova da sequentização.
Então, usamos alguns resultados obtidos para as proof-nets e apresentamos uma outra
abordagem para chegar à prova da sequentização para os N-Grafos. Usando a noção de subprovas,
definimos o império do norte, o do sul e o total (whole empire) de uma ocorrência de
fórmula A. Com isso, além da apresentação de uma nova prova de corretude para os N-Grafos
(sem o conectivo !), também é dado um método generalizado para realizar cortes precisos em
provas.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufpe.br:123456789/12419 |
| Date | 03 October 2013 |
| Creators | Carvalho, Ruan Vasconcelos Bezerra |
| Contributors | Oliveira, Anjolina Grisi de, Queiroz, Ruy José Guerra Barretto de |
| Publisher | Universidade Federal de Pernambuco |
| Source Sets | IBICT Brazilian ETDs |
| Language | Breton |
| 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 | Attribution-NonCommercial-NoDerivs 3.0 Brazil, http://creativecommons.org/licenses/by-nc-nd/3.0/br/, info:eu-repo/semantics/openAccess |
Page generated in 0.0026 seconds