Sistemas verificados para el razonamiento en la web semántica
Las actividades desarrolladas en el proyecto pueden clasificarse de acuerdo a dos líneas de trabajo: (1) el diseño de sistemas de razonamiento formalmente verificados que puedan aplicarse al razonamiento en la Web Semántica y (2) el desarrollo de metodologías automatizadas para la reparación de ontologías.
El punto de inicio de la primera línea de trabajo fue la verificación formal en ACL2 de un marco genérico para el desarrollo de demostradores proposicionales [1]. Este marco genérico puede instanciarse de manera automática para obtener demostradores ejecutables (y formalmente verificados). Entre las instancias, son destacables las que dan lugar a los tableros semánticos y el método de Davis-Putnam-Loveland.
El segundo problema que hemos estudiado es el equilibrio entre el esfuerzo de la verificación formal y la eficiencia de la implementación verificada; como caso de estudio hemos desarrollado una implementación ejecutable de un algoritmo de unificación cuadrático [C3.5, C3.6 y C6.2]. Las principales conclusiones del estudio son: (1) es posible obtener algoritmos eficientes formalmente verificados y (2) se ratifica la idea de que los algoritmos con estructuras de datos complejas y sofisticadas estructuras de control requieren más esfuerzos de verificación (en este trabajo hemos usado 214 definiciones y 775 teoremas en contraste con las 19 definiciones y 129 teoremas necesarios en la verificación de un algoritmo de unificación usando la representación prefija de términos).
El tercer problema que hemos estudiado es la formalización de la lógica descriptiva ALC en PVS [C3.9 y C6.4] y la construcción de demostradores para ALC formalmente verificados en PVS [C3.10 y C6.4]. Para la construcción de los demostradores hemos seguido la metodología de refinamientos sucesivos y hemos usado PVS-IO para obtener las versiones ejecutables. Este trabajo lo hemos desarrollado en tres fases. En la primera fase, hemos verificado formalmente en PVS un marco genérico para comprobar la satisfacibilidad en ALC. En la segunda fase, hemos implementado en PVS un algoritmo genérico correspondiente a la especificación del marco genérico previo, de forma que se conservan sus propiedades fundamentales. Para ello, hemos seguido una metodología de refinamientos formalizada en PVS en trabajos anteriores del grupo. Finalmente, en la tercera fase, hemos construido en PVS demostradores formalmente verificados para la lógica ALC, obtenidos como instancias del algoritmo genérico, al especificar la estrategia de aplicación de las reglas. Cabe destacar que la metodología desarrollada permite tanto la construcción de nuevos demostradores a partir del algoritmo genérico, como la implementación de nuevos algoritmos a partir del marco genérico, manteniendo siempre las propiedades verificadas en cada fase de la formalización.
En la segunda línea de trabajo, hemos analizado y sistematizado de tipo conceptual que pueden presentar las ontologías, utilizando el cálculo de conexión de regiones RCC como meta-ontología. Estos resultados se recogen en la Tesis de A.M. Chávez [C.2.1] y en [C3.3]. Además, en [C.2.1] estudiamos la reducción de varios problemas sobre anomalías en ontologías a problemas de razonamiento en retículos, susceptibles de ser tratados mediante técnicas de razonamiento automático [C3.1]. El problema de la deficiente expresividad-especificación de ontologías formales ha sido tratado en [C3.1] (expresividad) y en [C6.1] (incertidumbre provocada por la deficiente especificación de elementos de la ontología); el problema de la fusión de ontologías lo hemos tratado en [C6.3] y el problema de la extensión sugerida por los datos en [C3.7]. En los trabajos anteriores se formaliza una noción lógica de extensión robusta (retículo categoricidad) que nos permite utilizar técnicas de razonamiento automático. La metodología ha sido aplicada con éxito para la formalización del aprendizaje de servicios en el contexto de agentes basados en conocimiento [C6.6] y, convenientemente adaptada, se ha aplicado en la Tesis de A. Paredes [C2.2].
Finalmente, en [C3.4] hemos analizado, desde el punto de vista del razonamiento automático, los retos planteados por la reparación de ontologías. Además, proponemos una extensión de OWL para obtener demostradores especializados a partir de los marcos genéricos [1 y C3.10].
Referencias
Artículos anteriores
- F.J. Martín, J.A. Alonso, M.J. Hidalgo and J.L. Ruiz: Formal verification of a generic framework to synthesize SAT-provers. Journal of Automated Reasoning, Vol. 32, N. 4, 2004, pp. 287-313.
C2. Tesis doctorales realizadas total o parcialmente en el Proyecto
- C.2.1. Antonia M. Chávez González. Razonamiento mereotopológico automatizado para la depuración de ontologías (Universidad de Sevilla, 2002)
- C.2.2. Antonio Paredes Moreno. Técnicas de depuración e integración de ontologías en el ámbito empresarial (Universidad de Sevilla, 2004).
