Banca de DEFESA: LAURA FERNANDES DELL ORTO

Uma banca de DEFESA de MESTRADO foi cadastrada pelo programa.
DISCENTE : LAURA FERNANDES DELL ORTO
DATA : 15/02/2017
HORA: 09:00
LOCAL: Sala de Seminários do DMAT
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: 91
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, químicos 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, onde apresentamos detalhes que normalmente são omitidos. A partir do teorema de Eliminação do Corte, podemos concluir a consistência do sistema (para as lógicas que estamos utilizando) e outros resultados como a propriedade de subfórmula. O trabalho inicia-se com um capítulo de 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, apresenta-se a especificação de um sistema bioquímico utilizando SELL. Além disso, apresentamos 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
Externo à Instituição - MÁRIO SÉRGIO FERREIRA ALVIM - UFMG
Notícia cadastrada em: 06/02/2017 08:28
SIGAA | Superintendência de Tecnologia da Informação - | | Copyright © 2006-2023 - UFRN - sigaa20-producao.info.ufrn.br.sigaa20-producao