| |
|
Description: |
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 (\bot, \vee, \exists) 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".
Area(s): Logic and Computation
|
|
Date: |
|
| Start Time: |
17h |
|
Speaker: |
Gilda Ferreira (CMAF, UL)
|
|
Place: |
Sala 2.5
|
|
URL: |
http://www.mat.uc.pt/~kahle/seminario/
|
| Research Groups: |
-Algebra, Logic and Topology
|
|
See more:
|
<Main>
|
|
