Lógica linear como framework lógico
Lógica Linear; Framework; Eliminação do Corte; Multimodalidade; Coq
O uso da lógica linear como framework lógico consiste em: (1) incorporar sequentes de uma dada lógica objeto usando dois predicados na lógica linear que diferenciam fórmulas do lado esquerdo das fórmulas do lado direito; e (2) traduzir as regras do cálculo de sequentes da lógica objeto como teorias (cláusulas) da lógica linear. Se o conjunto de teorias possui certas características, podemos estabelecer resultados interessantes, como por exemplo a admissibilidade do corte, sem que seja necessário uma prova direta na lógica objeto. Usar a lógica linear como framework para raciocinar sobre diversos sistemas lógicos, em particular sistemas modais, e estabelecer traduções adequadas que obedeçam as características necessárias para concluir a admissibilidade do corte desses sistemas é o objetivo deste trabalho. Além de formalizar todos os resultados em um provador semiautomático de teoremas. Trata-se de uma pesquisa aplicada, de cunho descritivo, mediante revisão de estudos do uso da lógica linear como framework e extensão do framework. Destaca-se novos resultados de eliminação do corte para a lógica linear diretamente no sistema focado com e sem subexponeciais e construção de um framework baseado na lógica linear com multimodalidades mecanizados no provador de teoremas Coq.