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 [2, 3 y 4]. 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 [5 y 6] y la construcción de demostradores para ALC formalmente verificados en PVS [6 y 7]. Para la construcción de los demostradores hemos seguido la metodología de refinamientos sucesivos y hemos usado PVSio 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 [8] y en [9]. Además, en [8] 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 [10]. El problema de la deficiente expresividad-especificación de ontologías formales ha sido tratado en [10] (expresividad) y en [11] (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 [12] y el problema de la extensión sugerida por los datos en [13]. 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 [14] y, convenientemente adaptada, se ha aplicado en la Tesis de A. Paredes [15].

Finalmente, en [16] 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 7].

Referencias

1. 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.
2. J.L. Ruiz, F.J. Martín, J.A. Alonso y M.J. Hidalgo. Formal Correctness of a Quadratic Unification Algorithm. Journal of Automated Reasoning (2006) Vol 37 pp. 67–92.
3. D.A. Greve, M. Kaufmann, P. Manolios, J S. Moore, S. Ray, J.L. Ruiz–Reina, R. Sumners, D. Vroon y M. Wilding. Efficient Execution in an Automated Reasoning Environment. Journal of Functional Programming (2007) Vol. 18(1) pp. 15–46.
4. D.A. Greve, M. Kaufmann, P. Manolios, J S. Moore, S. Ray, J.L. Ruiz-Reina, R. Sumners, D. Vroon y M. Wilding. Efficient execution in an automated reasoning environment. Techical report TR–06–59, November 2006. Department of Computer Sciences, University of Texas at Austin.
5. J.A. Alonso, J. Borrego, M.J. Hidalgo, F.J. Martín y J.L. Ruiz. A Formally Verified Prover for the ALC Description Logic. TPHOLS 2007. Lecture Notes in Computer Science 4732 pp. 135-150.
6. J.A. Alonso, M.J. Hidalgo, F.J. Martín y J.L. Ruiz. Demostradores para la lógica descriptiva ALC formalmente verificados en PVS. Trabajo interno del Grupo de Lógica computacional, Sevilla 2007.
7. M.J. Hidalgo, J.A. Alonso, F.J. Martín y J.L. Ruiz. Constructing formally verified reasoners for the ALC description logic. Pendiente de publicación en Electronic Notes in Theoretical Computer Science (ENTCS, ISSN: 1571-0661).
8. A.M. Chávez Razonamiento mereotopológico automatizado para la depuración de ontologías. Tesis doctoral, Sevilla, 2005.
9. J. Borrego y A.M. Chávez Visual Ontology Cleaning: Cognitive Principles and Applicability. In “The Semantic Web: Research and Applications” (3rd European Semantic Web Conference, ESWC 2006 Budva, Montenegro, June 11-14, 2006 Proceedings). Lecture Notes in Computer Science, Vol. 4011, 2006, Springer, pp. 317–331.
10. J. Borrego y A.M. Chávez Extension of Ontologies Assisted by Automated Reasoning Systems. Lecture Notes in Computer Science. Vol. 3643, 2005. Pag. 247-253.
11. J. Borrego y A.M. Chávez Controlling Ontology Extension by Uncertain Concepts Through Cognitive Entropy . Proc. of ISWC'05 Workshop on Uncertainty Reasoning for the Semantic Web. pp. 56-66 (2005).
12. J. Borrego y A. M. Chávez Fusión automatizada de ontologías: Aplicación al razonamiento espacial cualitativo. Actas del Campus Multidisciplinar en Percepción e Inteligencia, CMPI–2006, Vol. I, pp. 91–102.
13. J. Borrego y A. M. Chávez A Formal Foundation for Knowledge Integration of Deficient Information in the Semantic Web. (EUROCAST 2007), Lecture Notes in Computer Science, Vol. 4739, 2007, Springer, pp. 305–312.
14. G.A. Aranda y J. Borrego Ontologías bajo Creative Commons. El futuro del conocimiento en la Web. Conferencia Internacional de Software Libre 3.0 (CISL 2007).
15. A. Paredes Técnicas de depuración e integración de ontologías en el ámbito empresarial. Tesis doctoral, Sevilla, 2007.
16. J.A. Alonso, J. Borrego A.M. Chávez y F.J. Martín Foundational Challenges in Automated Data and Ontology Cleaning in the Semantic Web. IEEE Intelligent Systems, 21(1):42-52 (2006).