Em direção a um cálculo de sequentes para a lógica de descrição ALCH

Abstract

A Lógica de Descrições é um dos formalismos usados para representar conhecimento de um domínio. A lógica de descrição pode ser entendida como um subconjunto da Lógica de Primeira Ordem e é equipada com uma semântica formal e uma sintaxe bem definida. O conhecimento representado em sistemas baseados em lógica de descrições pode ser validado através de diversos métodos, e esses métodos têm a capacidade de inferência para deduzir conhecimento implícito a partir dos conceitos e relações explicitamente representados. Um desses métodos de validação é o Cálculo de Sequentes. As provas geradas por esse método são consideradas de fácil compreensão. Isso é uma grande vantagem em relação a outros métodos de validação, pois a legibilidade/explicabilidade das provas é uma das partes mais fundamentais para um sistema de provas/deduções. Nesta dissertação, investigamos a teoria da prova para a lógica de descrição. Apresentamos um cálculo de sequentes para a DL ALCH e comparamos os resultados obtidos com outros cálculos de sequentes para a DL presentes na literatura.