Implementação de conversão de provas ALC para o cálculo de sequentes

Abstract

Em raciocínio automático, os usuários necessitam usar os sistemas de inferência não apenas para entender a conclusão resultante desse raciocínio, mas, também para saber como os sistemas chegaram naquelas conclusões, grande parte da legibilidade da prova é perdida para usuários que não possuem o domínio da lógica. O Método de Conexões realiza provas que são consideradas de difícil compreensão, pois, a matriz de prova gerada por esse método possui várias conexões que unem fórmulas atômicas complementares que são verificadas ao percorrer os caminhos da matriz. Este trabalho apresenta uma implementação do método de conversão das provas em 𝒜ℒ𝒞 geradas pelo método das conexões para um sistema de sequentes 𝒜ℒ𝒞, formalizado por Palmeira (2017). No processo de implementação, são codificadas as etapas propostas na formalização para gerar a prova no cálculo de sequentes em 𝒜ℒ𝒞. Com esse processo de conversão, é possível deixar a prova mais legível para usuários comuns, que podem ser detentores do conhecimento do domínio, apenas. O método implementado neste trabalho recebe a fórmula 𝒜ℒ𝒞, a correspondente prova de conexões em formato não-clausal e as suas conexões. Uma prova no Cálculo de Sequentes 𝒜ℒ𝒞 vai sendo construída e, por fim, é gerada a saída com a prova completa em sequentes. A expressividade da lógica de descrições 𝒜ℒ𝒞 é unida ao bom desempenho dos provadores automáticos de teorema, proporcionando uma saída mais amigável e compreensível do raciocínio automático.