Gilda Ferreira
(CMAF, UL)Introdução ao Cálculo de Dedução Natural - análise dos conectivos
Data: 15 de Outubro de 2007
Local: Sala 2.5
Hora: 17h
Resumo
O Cálculo de Dedução Natural, introduzido por Gerhard Gentzen em 1935
pretendendo aproximar-se o mais possível do modo de raciocínio humano, é
ainda hoje um dos sistemas formais dedutivos mais conhecidos e estudados.
Neste seminário propomo-nos introduzir, de modo sucinto, o Cálculo de Dedução
Natural e apresentar trabalho recente nesta área realizado em conjunto com
Fernando Ferreira. Mais especificamente, e na sequência de ser notório o
facto de alguns conectivos (⊥, ∨, ∃) estarem associados a regras
de eliminação de mais difícil tratamento, mostraremos uma forma de evitar
esses "maus" conectivos quando lidamos com o cálculo intuicionista de
predicados. Como consequência, pensamos ter obtido uma explicação bastante
natural para um tipo de transformações tradicionalmente introduzidas de modo
ad hoc: as "commuting conversions".
Este seminário é organizado com apoio do CMUC.
Reinhard Kahle.