Detalhes bibliográficos
| Ano de defesa: |
2017 |
| Autor(a) principal: |
SILVA, Eunice Palmeira da |
| Orientador(a): |
FREITAS, Frederico Luiz Gonçalves de |
| Banca de defesa: |
Não Informado pela instituição |
| Tipo de documento: |
Tese
|
| Tipo de acesso: |
Acesso aberto |
| Idioma: |
por |
| Instituição de defesa: |
Universidade Federal de Pernambuco
|
| Programa de Pós-Graduação: |
Programa de Pos Graduacao em Ciencia da Computacao
|
| Departamento: |
Não Informado pela instituição
|
| País: |
Brasil
|
| Palavras-chave em Português: |
|
| Link de acesso: |
https://repositorio.ufpe.br/handle/123456789/28362
|
Resumo: |
O método de conexões ganhou boa reputação na área de prova automática de teoremas por cerca de três décadas, devido à sua simplicidade, clareza, eficiência e uso racional de memória. Este método recentemente tem sido aplicado em provadores automáticos que raciocinam sobre ontologias escritas em lógica de descrições ℒ. No entanto, as provas geradas por esse método são de difícil compreensão, consistindo em um conjunto de pares de conexões que são formados por fórmulas atômicas complementares encontradas ao longo de cada caminho de uma matriz. A legibilidade das provas é em grande parte perdida pelo ganho de desempenho e transformações aplicadas à fórmula a ser provada. Esse trabalho apresenta um método de conversão das provas em ℒ geradas pelo método de conexões para um sistema de sequentes ℒ. Com a transformação para sequentes, obtém-se uma representação mais legível e inteligível. O método de conversão proposto aqui recebe a fórmula ℒ e sua correspondente prova de conexões em formato não-clausal. Uma representação em árvore da fórmula ℒ é construída e serve como guia no processo de conversão. À medida que a prova em conexões é percorrida, busca-se na árvore da fórmula os pares de literais complementares que formam as conexões; paralelamente a este processo, uma prova em sequentes vai sendo construída. Por fim, é apresentado o algoritmo que implementa o método de conversão, cuja complexidade sugere a viabilidade do método. |
