| Adolfo Gustavo Serra Seca Neto.
Um provador de teoremas multi-estratégia.
01/01/2007 |
| 1v.
181p.
Doutorado.
UNIVERSIDADE DE SÃO PAULO -
CIÊNCIAS DA COMPUTAÇÃO |
| Orientador(es): Marcelo Finger |
| Biblioteca Depositaria:
Biblioteca do IME |
|
|
|
| Palavras - chave: |
| Lógica, computação, provadores de teoremas |
|
|
| Área(s) do conhecimento: |
| LÓGICAS E SEMÂNTICA DE PROGRAMAS |
|
|
| Banca examinadora: |
|
|
|
|
| Mario Roberto Folhadela Benevides |
|
|
|
| Walter Alexandre Carnielli |
|
|
|
|
| Agência(s) financiadora(s) do discente ou autor tese/dissertação: |
|
|
|
|
|
| Dependência administrativa |
|
|
|
| Resumo tese/dissertação: |
| Nesta tese apresentamos o projeto e a implementação do KEMS, um provador de teoremas multi-estratégia baseado no método de tablôs KE. Um provador de teoremas multi-estratégia é um provador de teoremas onde podemos variar as estratégias utilizadas sem modificar o núcleo da implementação. Além de multi-estratégia, o KEMS é capaz de provar teoremas em três sistemas lógicos: lógica clássica proposicional, mbC e mCi. Listamos abaixo algumas das contribuições deste trabalho: * um sistema KE para mbC que é analítico, correto e completo; * um sistema KE para mCi que é correto e completo; * um provador de teoremas multi-estratégia com as seguintes características: - aceita problemas em três sistemas lógicos: lógica clássica proposicional, mbC e mCi; - tem seis estratégias implementadas para lógica clássica proposicional, duas para mbC e duas para mCi; - tem treze ordenadores que são usados em conjunto com as estratégias; - implementa regras simplificadoras para lógica clássica proposicional; - possui uma interface gráfica que permite a visualização de provas; - é de código aberto e está disponível na Internet em http://kems.iv.fapesp.br; * benchmarks obtidos através da comparação das estratégias para lógica clássica proposicional resolvendo várias famílias de problemas; - sete famílias de problemas para avaliar provadores de teoremas paraconsistentes; * os primeiros benchmarks para as famílias de problemas para avaliar provadores de teoremas paraconsistentes. |
|
|
