Seminários de Pesquisa do DAINF
(→Primeiro semestre de 2009) |
|||
| Linha 8: | Linha 8: | ||
| − | 22/04/2009 (quarta-feira) - 10:30 - "KEMS - Um provador de teoremas multi-estratégia" - Prof. [[Adolfo Neto]] | + | ==== 22/04/2009 (quarta-feira) - 10:30 - "KEMS - Um provador de teoremas multi-estratégia" - Prof. [[Adolfo Neto]] ==== |
Local: Mini-auditório (a confirmar). | 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. | 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]] | + | ==== 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. | ||
Clique [http://migre.me/hus aqui] para ler um artigo relacionado a esta palestra. | Clique [http://migre.me/hus aqui] para ler um artigo relacionado a esta palestra. | ||
Edição de 17h07min de 13 de abril de 2009
Tabela de conteúdo |
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. Clique aqui para ler um artigo relacionado a esta palestra.
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.
