Um estudo de lógica linear com subexponenciais - Orto, Laura Fernandes Dell (2017)
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.