Banca de QUALIFICAÇÃO: LAURA FERNANDES DELL ORTO

Uma banca de QUALIFICAÇÃO de MESTRADO foi cadastrada pelo programa.
DISCENTE : LAURA FERNANDES DELL ORTO
DATA : 25/11/2016
HORA: 08:00
LOCAL: Sala de seminários da Matemática CCET
TÍTULO:
Um estudo de Lógica Linear com Subexponenciais

PALAVRAS-CHAVES:
Lógica Matemática, Teoria da Prova, Eliminação do Corte, Lógica Linear, Lógica Linear com Subexponenciais

PÁGINAS: 85
RESUMO:
Em Lógica Clássica, podemos utilizar as hipóteses um número indeterminado de vezes. Por exemplo, a prova 
de um teorema pode fazer uso do mesmo lema várias vezes. Porém, em sistemas físicos e computacionais a
situação é diferente: um recurso não pode ser reutilizado após ser consumido em uma ação. Em Lógica Linear,
 fórmulas são vistas como recursos a serem utilizados durante a prova. É essa noção de recursos que faz a
Lógica Linear ser interessante para a modelagem de sistemas. Para tanto, a Lógica Linear controla o uso da
contração e do enfraquecimento através dos exponenciais ! e ?. Este trabalho tem como objetivo fazer um
estudo sobre a Lógica Linear com Subexponenciais (SELL), que é um refinamento da Lógica Linear. Em SELL,
os exponenciais da Lógica Linear possuem índices, isto é, ! e ? serão substituídos por !^i e ?^i, onde “i” é
um índice. Um dos pontos fundamentais de Teoria da Prova é a prova da Eliminação do Corte, que neste
trabalho é demonstrada tanto para Lógica Linear como para SELL. A partir do teorema de Eliminação do Corte,
 podemos concluir a consistência do sistema e outros resultados como a propriedade de subfórmula. O
trabalho inicia-se com um breve histórico da Lógica Matemática, depois se aprofunda em Teoria da Prova, e
em seguida se faz uma exposição sobre a Lógica Linear. Assim, com essas bases, apresenta-se a Lógica Linear
 com Subexponenciais. SELL tem sido utilizada, por exemplo, na especificação e verificação de diferentes
sistemas tais como sistemas bioquímicos, sistemas de interação multimídia e, em geral, em sistemas
concorrentes com modalidades temporais, espaciais e epistêmicas. Com essa base teórica bastante clara,
 pretende-se apresentar na defesa de dissertação a especificação de um sistema real (físico) ou um sistema
matemático (abstrato) utilizando SELL. Além disso, apresentaremos várias instâncias de SELL que tem
interpretações interessantes do ponto de vista computacional.

MEMBROS DA BANCA:
Presidente - 2114893 - CARLOS ALBERTO OLARTE VEGA
Interno - 1143603 - ELAINE GOUVEA PIMENTEL
Notícia cadastrada em: 26/10/2016 16:57
SIGAA | Superintendência de Tecnologia da Informação - | | Copyright © 2006-2023 - UFRN - sigaa27-producao.info.ufrn.br.sigaa27-producao