Título: Evaluación de demostradores de lógicas para la descripción sobre fórmulas híbridas
Autor: Alejandra Lorenzo
Directores: Mg. Gerardo Parra – Carlos Areces
Carrera: Licenciatura en Ciencias de la Computación
Fecha de defensa: 21 de Agosto de 2008
Resumen
En esta tesis presentamos una traducción de fórmulas híbridas a conceptos de lógica para la descripción, e implementamos dicha traducción para dos salidas distintas. Las sintaxis elegidas son la sintaxis del lenguaje de entrada de FaCT++ y la sintaxis OWL RDF/XML, utilizada por una gran variedad de demostradores de lógica para la descripción. Elegimos estas dos sintaxis, debido a que son las sintaxis utilizadas por FaCT++ y Pellet, dos razonadores de lógicas para la descripción que proveen el soporte para lógicas híbridas mínimo requerido para la implementación de la traducción: la posibilidad
de trabajar con nominales.
La implementación de nuestra traducción nos permitirá resolver problemas de lógica híbrida con herramientas de lógica para la descripción. Esta posibilidad es muy interesante, particularmente considerando que las lógicas para la descripción cuentan con mecanismos de inferencia muy experimentados. Pero más interesante aún es que dicha implementación nos dará la posibilidad de comparación entre demostradores de lógica híbrida y demostradores de lógicas para la descripción, algo que hasta ahora no se ha estudiado en profundidad y que puede ser de gran ayuda en el crecimiento de los demostradores involucrados.
Con este último objetivo en mente, comenzamos con la etapa de evaluaciones. En esta etapa utilizamos una herramienta de testeo originalmente desarrollada para el demostrador de lógica híbrida HyLoRes. Dicha herramienta ejecuta los tests generando fórmulas híbridas aleatoriamente por medio del generador de fórmulas híbridas aleatorias en CNF (forma normal conjuntiva), hGen. Estas fórmulas son entonces directamente procesadas por los razonadores de lógica híbrida hTab y HyLoRes, y traducidas a conceptos de lógicas para la descripción para ser luego procesadas por los razonadores
de lógicas para la descripción FaCT++ y Pellet. De esta forma podemos obtener una comparación entre todos los demostradores involucrados.
Los test preliminares que comenzamos a correr, y que analizamos en los capítulos finales de esta tesis, indican que es necesario tener particular cuidado con los operadores característicos de las lógicas híbridas. Durante nuestros tests, hemos observado que demostradores del estado del arte de lógicas de descripción como Fact++ y Pellet, tienen dificultades para decidir la satisfacibilidad de formulas híbridas.
