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.

Casamento de instâncias dentro de uma Ontologia - O caso das Produções Bibliográficas do Currículo Lattes

----------------------------------------------------------------------------
Seminário do Grupo de Lógica, Inteligência Artificial
e Métodos Formais - LIAMF
Seminário Registrado na CPG do IME/USP
Página: http://www.ime.usp.br/~liamf/seminarios/index.html
-----------------------------------------------------------------------------

Título: Casamento de instâncias dentro de uma Ontologia - O caso das Produções
Bibliográficas do Currículo Lattes

Palestrante: André Casado Castaño

Data:  dia 3.12.07 às 14:00 hs

Local: Sala 252 - Bloco A - IME - USP


Resumo:

Um dos problemas que pode-se ter dentro de uma ontologia é o de haver
múltiplas instâncias que representam um mesmo objeto.
Esse problema pode aparecer normalmente em qualquer ontologia por
diversas razões e estamos olhando em especial, neste estudo, as
ontologias criadas automaticamente através de scripts.
Mostraremos um pouco mais detalhadamente o problema das instâncias
múltiplas para o caso do Currículo Lattes, em especial para o problema
das produções bibliográficas dos pequisadores.
Será mostrada uma solução que está sendo implementada, segundo alguns
critérios específicos para o Currículo Lattes, para que
automaticamente sejam detectados objetos iguais e realizado o correto
casamento de instâncias, evitando problemas de duplicidades dentro da
ontologia.

Todos são bem-vindos!

MODALIDADES CATÓDICAS E ANÓDICAS

MODALIDADES CATÓDICAS E ANÓDICAS

Juliana Bueno-Soler
Programa de Pós-Graduação - IFCH/ UNICAMP
Grupo de Lógica Teórica e Aplicada - CLE/UNICAMP
 

RESUMO

Discutirei o papel da negação no âmbito das modalidades, tema central da
minha Tese de Doutorado, partindo das modalidades anódicas (sem negação) e
introduzindo gradativamente o elemento catódico (negações ) através das
LFI's (lógicas da inconsistência formal).

Mostrarei que resultados de completude e incompletude podem ser obtidos
para amplas classes de lógicas anódicas e catódicas axiomatizadas pelo
esquema geral de sistemas multimodais G^<a,b,c,d> combinados com LFI's,
com vistas também á obtenção de semânticas de traduções possíveis.

Avaliarei ainda a questão dos métodos de prova por tablôs e anéis de
polinômios para tais sistemas.
 

__._,_.___