English

CIn - Centro de Informática UFPE




Eventos Relacionados

Defesa de Tese de Doutorado Nº 380 "Conversão de Provas em Lógica de Descrições ALC Geradas pelo Método de Conexões para Sequentes"

A aluna Eunice Palmeira da Silva irá defender sua pesquisa no dia 15 de setembro, às 8h, no Anfiteatro. Início: 15/09/2017 às 08:00 Término: 15/09/2017 às 00:00 Local: Anfiteatro do CIn

Pós-Graduação em Ciência da Computação – UFPE

Defesa de Tese de Doutorado Nº 380

Aluno: Eunice Palmeira da Silva
Orientador: Prof. Frederico Luiz Gonçalves de Freitas
Co-orientador: Prof. Jens Otten (University of Oslo)
Título: Conversão de Provas em Lógica de Descrições ALC Geradas pelo Método de Conexões para Sequentes
Data: 15/09/2017
Hora/Local:  8h – Centro de Informática - Anfiteatro
Banca Examinadora:

Prof. Anjolina Grisi de Oliveira (UFPE / Centro de Informática)
Prof. Edward Hermann Haeusler (PUC-RJ / Departamento de Informática)
Prof. Ana Teresa de Castro Martins (UFC / Departamento de Computação)
Prof. Ivan José Varzinczak  (Université d’Artois & CNRS / Centre de Recherche en Informatique de Lens)
Prof. Evandro de Barros Costa  (UFAL / Instituto de Computação)


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 ALC. 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 performance e transformações aplicadas à fórmula a ser provada. Esse trabalho apresenta um método de conversão das provas em ALC geradas pelo método de conexões para um sistema de sequentes ALC. 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 ALC e sua correspondente prova de conexões em formato não-clausal. Uma representação em árvore da fórmula ALC é construída e serve como guia no processo de conversão. À medida em 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 processo, cuja complexidade sugere a viabilidade do método.

Palavras-chave: Lógica de Descrições, Attributive Concept Language with Complements (ALC), Método de Conexões, Cálculo de Sequentes.

  • © Centro de Informática UFPE - Todos os direitos reservados
    Tel +55 81 2126.8430 - Cidade Universitária - 50740-560 - Recife/PE
Plano4 Consultoria Web