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.

No description available.