Detalhes bibliográficos
| Ano de defesa: |
2017 |
| Autor(a) principal: |
Orto, Laura Fernandes Dell |
| Orientador(a): |
Vega, Carlos Alberto Olarte |
| Banca de defesa: |
Não Informado pela instituição |
| Tipo de documento: |
Dissertação
|
| Tipo de acesso: |
Acesso aberto |
| Idioma: |
por |
| Instituição de defesa: |
Não Informado pela instituição
|
| Programa de Pós-Graduação: |
PROGRAMA DE PÓS-GRADUAÇÃO EM MATEMÁTICA APLICADA E ESTATÍSTICA
|
| Departamento: |
Não Informado pela instituição
|
| País: |
Brasil
|
| Palavras-chave em Português: |
|
| Área do conhecimento CNPq: |
|
| Link de acesso: |
https://repositorio.ufrn.br/jspui/handle/123456789/22623
|
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. |
