A connection method for a defeasible extension of ALCH
Método de conexões, Lógicas de descrições, Raciocínio
anulável.
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 pápeis; (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.