Conversão de provas em lógica de descrições ALC geradas pelo método de conexões para sequentes

Abstract

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.