Detalhes bibliográficos
| Ano de defesa: |
2017 |
| Autor(a) principal: |
CARVALHO, Ruan Vasconcelos Bezerra |
| Orientador(a): |
OLIVEIRA, Anjolina Grisi de |
| Banca de defesa: |
Não Informado pela instituição |
| Tipo de documento: |
Tese
|
| Tipo de acesso: |
Acesso aberto |
| Idioma: |
por |
| Instituição de defesa: |
Universidade Federal de Pernambuco
|
| Programa de Pós-Graduação: |
Programa de Pos Graduacao em Ciencia da Computacao
|
| Departamento: |
Não Informado pela instituição
|
| País: |
Brasil
|
| Palavras-chave em Português: |
|
| Link de acesso: |
https://repositorio.ufpe.br/handle/123456789/28009
|
Resumo: |
Como verificar se uma prova clássica também é intuicionista? Em dedução natural basta não haver ocorrência da lei do terceiro excluído ou da eliminação da dupla negação, conforme proposto por Gentzen. No seu cálculo de sequentes o mesmo resultado é alcançado restringindo o número de fórmulas no lado direito a no máximo um. Assim não há múltiplaconclusão, embora esta seja importante para a simetria. Hoje já existem abordagens que levam isso em conta e propõem cálculos de sequentes para lógica intuicionista com várias fórmulas no consequente. Mas ainda que elas nos forneçam compreensões do que diferencia a lógica intuicionista da clássica, há o problema da burocracia inerente ao formalismo de Gentzen. Aqui separamos a lógica intuicionista da clássica em derivações não-sequenciais adotando uma abordagem geométrica. Propomos uma versão intuicionista para dois sistemas de múltipla conclusão inicialmente definidos apenas para a lógica clássica proposicional: os N-Grafos, apresentados por de Oliveira (2001) e baseado em dedução natural; e as proof-nets de Robinson (2003), inspiradas no cálculo de sequentes. |
