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