Razonamiento

El razonamiento en ontologías y bases de conocimiento es una de las razones por las que una especificación debe ser formal. Por razonamiento entendemos derivar hechos que no están expresados explícitamente en la ontología o en la base de conocimiento. Todos los formalismos que se han discutido en esta sección fueron creados con vistas al procesamiento automático, pero debido a sus propiedades, como la decidibilidad o la complejidad computacional, o incluso debido al nivel de formalidad, esto no siempre es posible. En esta sección discutiremos el razonamiento solo para las lógicas de descripción.

Las lógicas de descripción se crean con el objetivo de un razonamiento tratable. Algunos ejemplos de tareas requeridas a un razonador son los siguientes.

Satisfacibilidad de un concepto: determinar si una descripción del concepto no es contradictoria, es decir, si puede existir un individuo que sea instancia del concepto.
Subsunción de conceptos: determinar si el concepto C subsume al concepto D, es decir, si la descripción de C es más general que la descripción de D.
Consistencia de ABox con respecto a TBox: determinar si los individuos de ABox no violan las descripciones y axiomas descritos por TBox.
Comprobación de un individuo: comprobar si el individuo es instancia de un concepto
Recuperación de individuos: encontrar todos los individuos que son instancias de un concepto
Realización de un individuo: encontrar todos los conceptos a los que pertenece el individuo, especialmente los más específicos

Estas tareas no son semánticamente muy diferentes. Por ejemplo, la satisfacibilidad puede probarse como subsunción de ⊥: un concepto es insatisfacible si no puede existir ningún individuo que sea instancia de ese concepto. Para todas las tareas, es suficiente poder comprobar la consecuencia deductiva o derivar todas las consecuencias deductivas de una teoría. Sin embargo, puede haber algoritmos especiales optimizados para diferentes tareas dentro de un razonador.

La complejidad de algunas DL seleccionadas se muestra en la tabla siguiente; todas las lógicas de la tabla son decidibles. Incluso cuando la complejidad teórica parece ser intratable, existen razonadores optimizados que son utilizables en casos prácticos del mundo real.

Ejemplos de complejidad de las lógicas de descripción [DL complexity navigator]

Los algoritmos que se utilizan en razonadores implementados para calcular la subsunción pueden dividirse en dos grupos: estructurales y lógicos. Los algoritmos estructurales comparan la estructura sintáctica normalizada de los dos conceptos. Puede demostrarse que estos algoritmos son correctos; sin embargo, tienen problemas de completitud, especialmente cuando se usan lógicas más expresivas. Debido a este problema, hoy en día se usan casi exclusivamente algoritmos lógicos. Los algoritmos lógicos verifican la subsunción C⊑D comprobando que $C⊓¬D no sea satisfacible. Existen diferentes enfoques para verificarlo, incluida la traducción de la consulta a un razonador existente de lógica de predicados. El enfoque más dominante es el algoritmo tableau.

El algoritmo tableau intenta demostrar la satisfacibilidad de un concepto C construyendo un modelo, una interpretación I en la que D^I no esté vacía. Un tableau es un grafo que representa dicho modelo. En el grafo tableau, los nodos corresponden a individuos (elementos de Δ^I) y las aristas corresponden a relaciones entre individuos (elementos de Δ^IxΔ^I). El algoritmo comienza con un individuo que satisface D y aplica reglas de expansión hasta que ya no son posibles más inferencias o hasta que se encuentra una contradicción. Las reglas de expansión son específicas de una lógica de descripción particular y constan de dos partes. La cabecera de la regla establece las condiciones para aplicar la regla, y el cuerpo de la regla establece cómo expandir el tableau. Para más detalles, así como para otras técnicas destinadas a optimizar el rendimiento, véase nuevamente The Description Logic Handbook.