English

CIn - Centro de Informática UFPE




Eventos Relacionados

Defesa de tese de Doutorado N° 384 "Cálculos de Múltipla Conclusão para a Lógica Intuicionista sob uma Perspectiva Geométrica"

O aluno Ruan Carvalho irá defender sua pesquisa no dia 3 de novembro, ás 14h, no Anfiteatro. Início: 03/11/2017 às 14:00 Término: 03/11/2017 às 00:00 Local: Anfiteatro do CIn

Pós-Graduação em Ciência da Computação – UFPE

Defesa de Tese de Doutorado Nº  384

Aluno: Ruan Vasconcelos Bezerra Carvalho
Orientador: Profa. Anjolina Grisi de Oliveira
Título: Cálculos de Múltipla Conclusão para a Lógica Intuicionista sob uma Perspectiva Geométrica
Data: 03/11/2017
Hora/Local: 14h – Centro de Informática - Anfiteatro
Banca Examinadora:
Prof. Frederico Luiz Gonçalves de Freitas (UFPE / Centro de Informática)
Prof. Edward Hermann Haeusler (PUC/RJ / Departamento de Filosofia )
Prof. Luiz Carlos Pinheiro Dias Pereira ( PUC/RJ  -Departamento de Filosofia)
Prof. Gleifer Vaz Alves ( UTFPR / Departamento Acadêmico de Informática)
Prof. Benjamín René Callejas Bedregal  (UFRN) / Informática e Matemática Aplicada)


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últipla-conclusã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, apresentado por de Oliveira (2001) e baseado em dedução natural; e as proof-nets de Robinson (2003), inspiradas no cálculo de sequentes.

Palavras-chave: lógica intuicionista, grafos de prova, múltipla conclusão, teoria da prova, proof-nets

  • © Centro de Informática UFPE - Todos os direitos reservados
    Tel +55 81 2126.8430 - Cidade Universitária - 50740-560 - Recife/PE
Plano4 Consultoria Web