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.
segunda-feira, 3 de dezembro de 2007
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!
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
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.
sexta-feira, 23 de novembro de 2007
Lógicas rivais e a lógica paraconsistente
Título: Lógicas rivais e a lógica paraconsistente
Palestrante: Bruno Jacinto
Data: 28. 11 (quarta-feira)
Data: 28. 11 (quarta-feira)
Local: Sala de Seminários CLE - IFCH - UNICAMP
Horário: 16h
Horário: 16h
Resumo:
A análise realizada por Haack do conceito de lógicas rivais tem sido utilizado por alguns filósofos de modo a dar conta das intuições acerca dos tipos de diferenças entre lógicas, e atacado por outros, na medida em que não reflete tais intuições, resultando numa concepção de pouca relevância.
Apresentaremos uma clarificação do conceito, apontando algumas críticas aos critérios de identificação de lógicas como rivais propostos por Haack, mas defendendo a relevância filosófica do conceito tal como tratado pela filósofa.
Numa segunda parte da nossa exposição tomaremos por base a proposta apresentada para tentar definir a relação existente entre a lógica paraconsistente e a lógica clássica.
__._,_.___ Os Cursos de Metafísica de Kant
O Departamento de Filosofia da UFRN, através da Base de Pesquisa "Lógica, Conhecimento e Ética", dá continuidade à programação de seus Seminários de Lógica e Filosofia Formal, com a palestra
Os Cursos de Metafísica de Kant
Profa. Dra. Juan A. Bonaccini -DeFIL - UFRN
Data: 30 / 11 /2007 às 16 h
Local: UFRN / CCHLA / Auditório de Filosofia
Os Cursos de Metafísica de Kant
Profa. Dra. Juan A. Bonaccini -DeFIL - UFRN
Data: 30 / 11 /2007 às 16 h
Local: UFRN / CCHLA / Auditório de Filosofia
quinta-feira, 22 de novembro de 2007
Soluções aproximadas para um MDPIP fatorado
----------------------------------------------------------------------------
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: Soluções aproximadas para um MDPIP fatorado
Palestrante: Karina Valdivia Delgado
Data: dia 26.11.07 às 14:00 hs
Local: Sala 252 - Bloco A - IME - USP
Resumo:
O tema principal desse seminário está relacionado à área de planejamento sob incerteza da Inteligência Artificial (IA). Trabalhos recentes nessa área adotam modelos estocásticos, com soluções bem conhecidas. No entanto, modelos com informação incompleta são de grande interesse na área de IA por serem mais aplicáveis em problemas práticos. Nesse seminário, fazemos uma breve revisão dos principais conceitos da área de processos Markovianos de Decisão (MDPs) e apresentamos um algoritmo aproximado baseado em programação linear, para resolver MDPs fatorados (isto é, uma representação compacta para MDPs que envolvam um grande número de estados). Em seguida, definimos um MDP impreciso (MDPIP), isto é, um MDP em que as distribuições de probabilidade sob as transições de estado não são completamente conhecidas. O objetivo desse seminário é propor diferentes soluções aproximadas para um MDPIP fatorado, uma vez que não são conhecidas soluções na literatura para esse problema.
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: Soluções aproximadas para um MDPIP fatorado
Palestrante: Karina Valdivia Delgado
Data: dia 26.11.07 às 14:00 hs
Local: Sala 252 - Bloco A - IME - USP
Resumo:
O tema principal desse seminário está relacionado à área de planejamento sob incerteza da Inteligência Artificial (IA). Trabalhos recentes nessa área adotam modelos estocásticos, com soluções bem conhecidas. No entanto, modelos com informação incompleta são de grande interesse na área de IA por serem mais aplicáveis em problemas práticos. Nesse seminário, fazemos uma breve revisão dos principais conceitos da área de processos Markovianos de Decisão (MDPs) e apresentamos um algoritmo aproximado baseado em programação linear, para resolver MDPs fatorados (isto é, uma representação compacta para MDPs que envolvam um grande número de estados). Em seguida, definimos um MDP impreciso (MDPIP), isto é, um MDP em que as distribuições de probabilidade sob as transições de estado não são completamente conhecidas. O objetivo desse seminário é propor diferentes soluções aproximadas para um MDPIP fatorado, uma vez que não são conhecidas soluções na literatura para esse problema.
domingo, 11 de novembro de 2007
Desktops Semânticos
----------------------------------------------------------------------------
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: Desktops semânticos
Palestrante: Rodrigo Rage Ferro
Data: dia 12.11.07 às 14:00 hs
Local: Sala 252 - Bloco A - IME - USP
Resumo:
A quantidade crescente e a diversidade de dados armazenados em computadores fazem a organização e a localização da informação uma tarefa difícil. Usuários tentam por meio de uma estrutura de diretórios realizar a organização dos arquivos. Infelizmente, o sistema tradicional hierárquico de arquivos não está conseguindo mais atender de forma satisfatória este propósito. A tarefa de localizar então torna-se penosa, fazendo com que muitas vezes seja mais cômodo para o usuário usar ferramentas de busca na Web do que procurar o arquivo no seu próprio HD. Tentando integrar Web Semântica com aplicações de desktop, surge o chamado Semantic Desktop.
Entre os objetivos do desktop semântico está vincular o arquivo com a informação contextual obtida no momento em que ele é usado/salvo por meio de metadados em RDF. Assim, quando o usuário busca por um arquivo espera-se, que mais do que palavras-chave, uma semântica seja explorada de forma a restringir e tornar mais eficiente o processo de busca.
Nessa apresentação, será abordado sobre Semantic Desktop: objetivos, arquitetura típica e projetos existentes, além de como web semântica pode auxiliar nesse processo de busca mais eficiente.
Todos são bem-vindos!
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: Desktops semânticos
Palestrante: Rodrigo Rage Ferro
Data: dia 12.11.07 às 14:00 hs
Local: Sala 252 - Bloco A - IME - USP
Resumo:
A quantidade crescente e a diversidade de dados armazenados em computadores fazem a organização e a localização da informação uma tarefa difícil. Usuários tentam por meio de uma estrutura de diretórios realizar a organização dos arquivos. Infelizmente, o sistema tradicional hierárquico de arquivos não está conseguindo mais atender de forma satisfatória este propósito. A tarefa de localizar então torna-se penosa, fazendo com que muitas vezes seja mais cômodo para o usuário usar ferramentas de busca na Web do que procurar o arquivo no seu próprio HD. Tentando integrar Web Semântica com aplicações de desktop, surge o chamado Semantic Desktop.
Entre os objetivos do desktop semântico está vincular o arquivo com a informação contextual obtida no momento em que ele é usado/salvo por meio de metadados em RDF. Assim, quando o usuário busca por um arquivo espera-se, que mais do que palavras-chave, uma semântica seja explorada de forma a restringir e tornar mais eficiente o processo de busca.
Nessa apresentação, será abordado sobre Semantic Desktop: objetivos, arquitetura típica e projetos existentes, além de como web semântica pode auxiliar nesse processo de busca mais eficiente.
Todos são bem-vindos!
Assinar:
Postagens (Atom)