English

CIn - Centro de Informática UFPE




Eventos Relacionados

Defesa de Dissertação de Mestrado nº 1341: "Uma nova prova de corretude para os N-Grafos"

O aluno Ruan Vasconcelos Bezerra Carvalho irá defender seu trabalho dia 3 de outubro, às 8h, no Anfiteatro Início: 03/10/2013 às 08:00 Término: 03/10/2013 às 10:00 Local: Anfiteatro do CIn

Pós-Graduação em Ciência da Computação – UFPE
Defesa de Dissertação de Mestrado nº 1341
 
Aluno: Ruan Vasconcelos Bezerra Carvalho
Orientador: Profa. Anjolina Grisi de Oliveira
 
Título: Uma nova prova de corretude para os N-Grafos
Data: 03/10/2013
Hora/Local: 08h – Anfiteatro 
 
Banca Examinadora:
Prof. Frederico Luiz Gonçalves de Freitas (UFPE / CIn)
Prof. Luiz Carlos Pinheiro Dias Pereira (PUC-Rio – Deptº de Filosofia)
Prof. Anjolina Grisi de Oliveira (UFPE / CIn)
 
RESUMO:
 
Desde que proof-nets para MLL- foram introduzidas por Girard, vários estudos foram realizados na prova de corretude delas. O primeiro critério foi "no shorttrip condition": Girard usou trips para definir impérios e provou que se todas as fórmulas terminais numa proof-net R forem conclusões de links times ou de axiomas, então pelo menos um link terminal divide R em duas partes (o "nó split"). Outro avanço na prova de corretude 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 sequencialização utilizando propriedades simples das subnets e mostrando como encontrar o nó split. Todavia, estas abordagens não se aplicam aos N-Grafos, uma vez que a noção de reinos não pode ser empregada no sistema. Não obstante, a necessidade de identificar a nó split está no coração da prova da sequencialização. Então é preciso outra abordagem para chegar à prova da sequancialização para os N-Grafos usando a noção de subprovas: definiremos o império do norte, do sul e o total (whole empie) de uma ocorrência de fórmula. Com isso, além da apresentação de uma nova prova de corretude para os N-Grafos (sem o conectivo de implicação), também é dado um método generalizado para realizar cortes precisos em provas.
 
 
Palavras-chave: N-Grafos, dedução natural, cálculo de sequentes, MLL-, subnets. 
  • © Centro de Informática UFPE - Todos os direitos reservados
    Tel +55 81 2126.8430 - Cidade Universitária - 50740-560 - Recife/PE
Plano4 Consultoria Web