KEMS - Um provador de teoremas multi-estratégia

Programação do 1º semestre de 2009:

http://www.dainf.ct.utfpr.edu.br/wiki/index.php/Semin%C3%A1rios_de_Pesquisa_do_DAINF

SÉRIE DE SEMINÁRIOS DE PESQUISA DO DAINF

             ***** 2ª PALESTRA *****

            DAINF - UTFPR

Data:   22 DE ABRIL de 2009, QUARTA-FEIRA
Hora:  10:30h
Local: Mini-Auditório da UTFPR - Campus Curitiba

Palestrante: Prof. Adolfo Neto (DAINF-UTFPR)

Titulo: "KEMS - Um provador de teoremas multi-estratégia"

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. Falaremos também um pouco sobre a implementação do KEMS, que foi feita em Java e AspectJ (uma linguagem orientada a aspectos), usando algumas técnicas usadas em métodos ágeis de desenvolvimento de software.

Mini-CV: Adolfo Neto é Doutor em Ciências da Computação pela Universidade de São Paulo (USP), Mestre em Ciência da Computação pela Universidade Federal de Pernambuco (UFPE) e bacharel em Ciências da Computação pela Universidade Federal de Alagoas (UFAL). Atualmente é professor do Departamento de Informática (DAINF) da Universidade Tecnológica Federal do Paraná (UTFPR), Campus Curitiba. Foi professor da Universidade do Estado de Santa Catarina (UDESC), do Centro Federal de Educação Tecnológica de São Paulo (CEFET-SP), da Pontifícia Universidade Católica de Campinas (PUC-CAMPINAS), do Centro Federal de Educação Tecnológica de Alagoas (CEFET-AL) e da Universidade Federal de Alagoas. Foi analista desenvolvedor de sistemas na Inmetrics, uma empresa de soluções em serviços de APM.

Tem experiência na área de Ciência da Computação, com ênfase em Lógica Aplicada à Computação, atuando principalmente nos seguintes temas: sistemas de prova baseados em tablôs, prova automática de teoremas, e lógicas paraconsistentes. Tem, também, interesse em métodos ágeis para o desenvolvimento de software.

Todos são bem-vindos!!!