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. |
