segunda-feira, 3 de dezembro de 2007

SEMANA DA LÓGICA, na UFRN (2007.2)

Mais uma realização do grupo de pesquisa da UFRN em
"Lógica e Filosofia Formal".

Estão todos convidados!

Tema: Fundamentos da demonstração automática de teoremas
Palestrante: João Marcos
Data de realização: 10/12/07, 2a-feira, 18h30
Local: anfiteatro B do CCET
Resumo:
Esta palestra fará uma breve introdução histórica e conceitual à área de demonstração assistida ou automática de teoremas. Os fundamentos teóricos relacionados à programação funcional e à lógica de ordem superior servirão de base para uma apresentação ao ambiente computacional de demonstração *Isabelle*.

Tema: Matemática Discreta Aplicada
Palestrante: Lucas Cavalcante
Data de realização: 11/12/07, 3a-feira, 18h30
Local: anfiteatro B do CCET
Resumo:
Nesta palestra veremos como lidar com objetos fundamentais da Matemática Discreta no ambiente de demonstração assistida de teoremas *Isabelle*. O objetivo é expor uma similaridade entre demonstrações implementadas com o auxílio da ferramenta *Isabelle* e aquelas realizadas da maneira usual, à mão. Abordaremos conceitos como funções recursivas, conjuntos parcialmente ordenados, princípio da indução e estruturas de dados em forma de listas.

Tema: Dedução Natural em *Isabelle*
Palestrante: Dalmo Mendonça
Data de realização: 12/12/07, 4a-feira, 18h30
Local: anfiteatro B do CCET
Resumo:
Demonstrações de teoremas por dedução natural no sistema *Isabelle* podem ser feitas da maneira usual: aplicando regras de inferência. A garantia da correção é um ponto forte do sistema. Será apresentada a teoria correspondente à Lógica Clássica Proposicional e será mostrado como criar regras de inferências derivadas e regras de abreviatura. A maior vantagem do *Isabelle* aparece no uso de técnicas avançadas, os taticais, que são comandos que permitem automatizar parcialmente ou totalmente as demonstrações.

Tema: Uma introdução ao Cálculo Lambda
Palestrante: Talis Lincoln
Data de realização: 13/12/07, 5a-feira, 16h30
Local: anfiteatro B do CCET
Resumo:
Nesta palestra será apresentado o Cálculo Lambda, um sistema formal desenvolvido para estudar definições e aplicações de funções. Mostraremos conceitos, regras, definições e notações do Cálculo Lambda. Serão discutidos ainda as grandes semelhanças com linguagens de programação funcional, em particular SML, e a estreita relação existente entre programas de computador e demonstrações matemáticas, fenômeno conhecido como isomorfismo de Curry-Howard.

Um comentário:

Anônimo disse...
Este comentário foi removido por um administrador do blog.