KEMS - Provador de Teoremas Multi-Estratégia
O KEMS é um provador de teoremas multi-estratégia baseado no método KE. O sistema KE, um método de tablôs desenvolvido por Marco Mondadori e Marcello D'Agostino [1], foi apresentado como uma melhoria, no sentido da eficiência computacional, em relação ao método dos Tablôs Analíticos [2]. 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 Gustavo Serra Seca Neto, que foi orientado por Marcelo Finger. KEMS foi implementado em Java e AspectJ. Java é uma linguagem de programação orientada a objetos bastante usada enquanto AspectJ é a principal representante de um novo paradigma de programação: programação orientada a aspectos.
[1] The Taming of the Cut. Classical Refutations with Analytic Cut Journal of Logic and Computation, vol. 4, number 3, pp. 285-319, 1994
[2] First-Order Logic, Raymond Smullyan. Dover Publications, 1968
Maiores informações em http://adolfoneto.wikidot.com/kems
Avaliação
O KEMS foi avaliado utilizando famílias de problemas difíceis.
