Pós-Graduação em Ciência da Computação – UFPE
Defesa de Tese de Doutorado Nº 639
Aluno: Renan Leandro Fernandes
Orientador: Prof. Frederico Luiz Gonçalves de Freitas
Coorientador: Prof. Ivan José Varzinczak (Laboratoire d’Intelligence Artificielle et Sémantique des Données – LIASD)
Título: A connection method for a defeasible extension of ALCH
Data: 30/08/2024
Hora/Local: 13:30 – Virtual – Interessados em assistir entrar em contato com o aluno
Banca Examinadora:
Prof. Anjolina Grisi de Oliveira (UFPE / Centro de Informática)
Prof. Renata Wassermann (USP / Instituto de Matemática e Estatística)
Prof. Cláudia Nalon (UnB / Departamento de Ciência da Computação)
Prof. Ruan Vasconcelos Bezerra Carvalho (UFRPE / Departamento de Computação)
Prof. Pedro Porfirio Muniz Farias (UNIFOR/Diretoria do Centro de Ciências Tecnológicas)
RESUMO:
A modelagem de exceções em ontologias e o raciocínio em sua presença recebeu uma significante atenção na última década. O desenvolvimento de métodos de prova para as Lógicas de Descrições (DLs) anuláveis, seguindo os métodos para as DLs clássicas, é principalmente baseado em tableaux semânticos. No entanto, a literatura apresenta alternativas igualmente viáveis para provadores de teoremas automáticos, como o método de conexões. Este método consiste em um algoritmo de busca de prova orientado à um objetivo, buscando por conexões (pares de literais complementares) em conjuntos de cláusulas de literais chamada de matriz. Esta tese apresenta um método de conexões para uma família de DLs tolerante à exceções. Nesse sentido, este trabalho apresenta as seguintes contribuições: (i) investigação da linguagem DL ALCH, estendida com operadores de tipicalidade nos conceitos e nos papéis; (ii) revisitação da definição de uma representação matricial de uma base de conhecimento e estabelece condições para que um dado axioma seja provado pela matrix; (iii) apresentação do tratamento de unificação de termos e definição de uma condição de bloqueio ajustável na presença de operadores de tipicalidade; (iv) fornecimento de uma ligação entre estruturas matriciais e a semântica de DLs anuláveis; (v) provas de corretudo, completude e terminação para o sistema de inferência proposto, dependendo apenas da semântica das lógicas de descrições anuláveis; e (vi) um provador de métodos de conexões polimórfico, o Java-CoP, desenvolvido para a linguagem ACLHb e que, no entanto, pode abranger possivelmente qualquer outra lógica, com modificações sutis em seus métodos e classes.
Palavras-chave: Método de conexões, Lógicas de descrições, Raciocínio anulável.
Comentários desativados