Un algoritmo en seudocodigo para el chequeo de la subsumicion en alc Un algoritmo en seudocodigo para el chequeo de la subsumicion en alc

Resumen

En el presente artículo se describe un evaluador de satisfactibilidad para el chequeo de la subsumición en un lenguaje de atributos de conceptos (Attribute Language Concept, ALC). Los lenguajes de conceptos basados en las lógicas descriptivas (Description Logics, DLs) ofrecen servicios de razonamiento que permiten hacer clasificación y recuperación de la información dentro de la base de conocimiento. Los procesos de razonamiento de subsumición y de satisfactibilidad son equivalentes y se especifican por medio del Cálculo de Predicados de Primer Orden (First Order Predicate Calculus, FOPC) y el cálculo Tableaux. FOPC permite asociar cada expresión C de conceptos a una fórmula f c (x) de la lógica de predicados, de tal forma que un modelo de una fórmula f c (x) es un modelo del concepto C y viceversa. El cálculo Tableaux de primer orden siempre termina para las fórmulas asociadas a conceptos en el FOPC. El cálculo de terminación planteado permite una interpretación si la fórmula es satisfactible o se produce una contradicción si la fórmula es insatisfactible. Se plantea un algoritmo en seudocódigo para el chequeo de la subsumición.