Seminários de Pesquisa do DAINF

Edição de 17h43min de 13 de abril de 2009

Descrição

Ciclo de apresentações de temas de pesquisa no DAINF.

Programação

Primeiro semestre de 2009

22/04/2009 (quarta-feira) - 10:30 - "KEMS - Um provador de teoremas multi-estratégia" - Prof. Adolfo Neto

Local: Mini-auditório (a confirmar).

Resumo: O KEMS (http://www.dainf.ct.utfpr.edu.br/~adolfo/KEMS) é um provador de teoremas multi-estratégia baseado no método KE. O sistema KE é um método de tablôs que foi apresentado como uma melhoria, no sentido da eficiência computacional, em relação ao método dos Tablôs Analíticos. Um provador de teoremas multi-estratrégia é um provador de teoremas no qual podemos variar a estratégia sem modificar o núcleo da implementação. Um provador de teoremas multi-estratégia pode ser utilizado com três propósitos: educacional, exploratório e adaptativo. Para fins educacionais, o KEMS pode ser usado para ilustrar como a escolha da estratégia de prova pode afetar a performance de um provador de teoremas. Como uma ferramenta exploratória, um provador de teoremas multi-estratégia pode ser usado para testar novas estratégias e compará-las com outras existentes. E podemos pensar também em um provador de teoremas multi-estratégia adaptativo que modifique a estratégia usada de acordo com as características do problema apresentado ao provador. O KEMS foi implementado durante o doutorado de Adolfo Neto, que foi orientado por Marcelo Finger. Nesta palestra discutiremos as contribuições do KEMS na área de Lógica para Computação.

06/04/2009 (segunda-feira) - 14:00 - "Classificação Automática de Gêneros Musicais" - Prof. Celso Kaestner

Local: Sala de vídeo conferência.

Resumo: O tema a ser apresentado é a classificação automática de gêneros musicais a partir de arquivos em formato digital (MP3 ou similar). Inicialmente os arquivos são tratados por procedimentos de extração, que geram vetores de características. Estes vetores são então submetidos a algoritmos de aprendizagem de máquina, seguindo o paradigma supervisionado para problemas de classificação. No projeto empregou-se uma abordagem baseada na cooperação de diversos classificadores, seguindo a decomposição do problema nas dimensões "espacial" e "temporal". São empregados diversos classificadores: naïve-Bayes, árvores de decisão, SVM, redes neurais e k-NN. Foram também realizados experimentos de seleção de atributos, com o uso de um procedimento baseado em algoritmos genéticos. Todos os experimentos empregaram uma nova base de dados, a "Latin Music Database", composta por 3.160 músicas de 10 gêneros musicais.

Slides de "Classificação Automática de Gêneros Musicais" - Prof. Celso Kaestner (em PDF)

Clique aqui para ler um artigo relacionado a esta palestra.

Sugestões para Futuras Palestras