| |
|
Description: |
A dedução natural e o cálculo de sequentes são dois dos principais sistemas de dedução formal usados e estudados em teoria estrutural da demonstração. A dedução natural manipula fórmulas, procura modelar o
raciocínio informal usado, por exemplo, nas demonstrações matemáticas, e tem relações priveligiadas com o lambda-calculus e, por via deste, com a programação funcional. O cálculo de sequentes manipula instâncias formais da relação de consequência lógica, procura modelar uma dualidade entre hipótese e conclusão, e é especialmente adequado
para a busca semi-automática de demonstrações, tendo, por isso, relações priveligiadas com a programação em lógica. A investigação das últimas décadas mostrou que estas e outras diferenças são mais aparentes do que reais. Neste seminário vamos ilustrar alguns resultados recentes e, de algum modo radicais, neste processo de "unificação". Estes resultados obtêm-se a partir do momento em que se compreende a relação do cálculo de sequentes com o lambda-calculus, e desde que se esteja preparado para aceitar um alargamento do conceito de dedução natural.
Area(s): Logic and Computation
|
|
Date: |
|
| Start Time: |
16:00 |
|
Speaker: |
José Carlos Espírito Santo (Dep. Matemática, Univ. Minho)
|
|
Place: |
Sala 5.5
|
| Research Groups: |
-Algebra, Logic and Topology
|
|
See more:
|
<Main>
|
|
