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

Detalhes bibliográficos
Ano de defesa: 2019
Autor(a) principal: SILVA, Allison Magno Eugênio da
Orientador(a): FREITAS, Frederico Luiz Gonçalves de
Banca de defesa: Não Informado pela instituição
Tipo de documento: Dissertação
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/37645
Resumo: 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.