Resolución con orden y selección para la lógica H(@)

Daniel Alejandro Gorín (1), Carlos Eduardo Areces (2)

e-mails: email@domain, email@domain

(1) Facultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires Ciudad Universitaria - Pabellón I (1428) Buenos Aires Argentina
(2) INRIA Lorraine 615, Rue du Jardin Botanique 54602 Villers les Nancy Cedex Francia

Abstract

Las lógicas modales son reconocidas por combinar buenas propiedades computacionales (e.g. decidibilidad) con un alto poder expresivo. Estas propiedades han sido explotadas con éxito en Computación; un caso paradigmático lo constituyen las description logics (DLs), una familia de lógicas modales utilizadas en la construcción de sistemas de representación de conocimiento (knowledge representation systems o KRS). En este tipo de sistemas se puede dar una descripción conceptual de un universo junto con una enumeración de los elementos que lo constituyen, y a partir de ahí, inferir información que no se encuentra declarada en forma explícita. Este tipo de sistemas se utilizan, por ejemplo, en Inteligencia Artificial y en Linguística Computacional, y han sido propuestos como base para el lenguaje de representación de ontologías que se usaría en la Web Semántica [4].

Las lógicas modales tradicionales, sin embargo, no permiten hacer referencia a elementos particulares del modelo, ni permiten tampoco representar igualdades. La lógica híbrida H(@) es la que se obtiene al agregar nominales y el operador de satisfacción @ a la lógica modal básica. Los nominales permiten nombrar elementos del modelo y junto con el operador @ incorporan una noción débil de igualdad. A pesar de su mayor poder expresivo, H(@) sigue siendo decidible: de hecho, su complejidad para el problema de la satisfaciblidad es igual al de la lógica modal básica, PSPACE-completo.

Habitualmente, los demostradores de teoremas para las lógicas modales están basados en algoritmos de tableau que, combinados con diversas heurísticas y optimizaciones, muestran buen comportamiento empírico. Sin embargo, muchas de estas heurísticas no son correctas cuando la lógica incorpora igualdad. Es interesante, entonces, investigar qué sucede con otras familias de algoritmos.

En [2] se propone un cálculo basado en resolución para H(@). Este cálculo, si bien consistente y completo, carece de las estrategias de orden y selección que son parte esencial de los demostradores para lógica de primer orden basados en resolución. Una implementación computacionalmente realista de un demostrador basado en resolución requiere de este tipo de estrategias para regular la generación desproporcionada de nuevas cláusulas y como guía dentro de un espacio de búsqueda extremadamente complejo.

El primer resultado de esta tesis es la definición de una estrategia de orden y selección muy general para el cálculo de resolución propuesto en [2], que preserva completitud refutacional (i.e., si bien el espacio de búsqueda disminuye drásticamente, el algoritmo de refutación sigue siendo correcto y completo). Como un paso necesario para la demostración general de completitud, se presenta un Teorema de Herbrand [11] para la lógica H(@). Este resultado permite reducir el problema de satisfacibilidad sobre la clase de todos los modelos posibles a la subclase de los modelos de Herbrand (este es, hasta donde sabemos, el primer resultado de este tipo para lógicas modales).

El segundo resultado que la tesis presenta es una demostración de terminación para el cálculo propuesto previamente. Tomando ventaja de la generalidad de la demostración anterior, podemos modificar el cálculo para asegurar terminación dada cualquier entrada. Si bien en [1] se demuestra que la complejidad del problema de satisfacibilidad para H(@) es PSPACE-completo (y por lo tanto decidible), nuestra demostración provee el primer algoritmo computacionalmente realizable.

Por último, los resultados teóricos de esta tesis fueron puestos a prueba en la re-implementación del prototipo HyLoRes, un demostrador automático basado en el cálculo de [2]. Los tests que presentamos muestran claramente que las estrategias de orden y selección también producen una mejora drástica en un algoritmo de resolución para lógicas híbridas, obteniendo tiempos de cómputo varios órdenes de magnitud menores.

Keywords:Logica Modal, Lógica Híbrida H(@)

BibTex

@INPROCEEDINGS{gorin04:402,
                  AUTHOR       = {Daniel Alejandro Gorín and Carlos Eduardo Areces},
                  TITLE        = {Resolución con orden y selección para la lógica H(@)},
                  BOOKTITLE    = {30ma Conferencia Latinoamericana de Informática (CLEI2004)},
                  YEAR         = {2004},
                  editor       = {Mauricio Solar and David Fernández-Baca and Ernesto Cuadros-Vargas},
                  pages        = {1179--1199},
                  address      = {},
                  month        = Sep,
                  organization = {Sociedad Peruana de Computación},
                  note         = {ISBN 9972-9876-2-0},
                  file         = {http://clei2004.spc.org.pe/es/html/pdfs/402.pdf}
}

PDF de este artículo
PDF de CLEI2004 (incluye todos los artículos)
Página principal CLEI 2004
Generado por Sociedad Peruana de Computación