Advanced evaluation techniques for (non)-monotonic reasoning using rules with constraints

• Autores: Joaquin Arias Herrero
• Directores de la Tesis: Manuel Carro Liñares (dir. tes.)
• Lectura: En la Universidad Politécnica de Madrid ( España ) en 2020
• Idioma: español
• Tribunal Calificador de la Tesis: Gopal Gupta (presid.) , Julio Mariño Carballo (secret.) , Pedro Cabalar (voc.) , Agostino Dovier (voc.) , José Francisco Morales Caballero (voc.)
• Enlaces
  • Tesis en acceso abierto en: Archivo Digital UPM
• Resumen

  • La programación lógica con restricciones (CLP) es un paradigma de programación declarativa que extiende la programación lógica (LP) con capacidades para resolver restricciones sobre diferentes dominios que puede combinarse para modelar el problema a resolver. CLP aporta mayor expresividad a LP, ya que las restricciones pueden representar relaciones complejas de manera concisa. Esto simplifica el desarrollo de programas que resuelven problemas para los que no existe un algoritmo eficaz y/o la adaptación de dichos programas cuando las especificaciones del problema cambian. Además, al cambiar de "generar y probar" a "restringir y generar" se reduce el árbol de búsqueda y se incrementa la eficiencia. CLP se ha utilizado, entre otras aplicaciones, en planificación, asignación de recursos, logística, diseño de circuitos y verificación. Sin embargo, una estrategia de ejecución top-down de CLP puede entrar en bucle debido a la recursión por la izquierda y/o la presencia de negación no estratificada, mientras que una estrategia de ejecución bottom-up limita el rango de dominios de restricción admisibles, donde pueden aparecer las restricciones y el tipo (o número) de modelos que se pueden obtener.

    Esta tesis contribuye al estado del arte de la programación lógica con restricciones y tabulación (TCLP), que suspende llamadas más particulares comprobando entailment (haciendo que los programas CLP terminen en más casos), y de la programación lógica con restricciones con conjuntos de respuestas (Constraint Answer Set Programming, CASP), que evalúa programas CLP con negación usando la semántica de modelos estables.

    En primer lugar, ampliamos los fundamentos teóricos de TCLP, demostrando corrección y completitud de una semántica operacional top-down de TCLP que utiliza una estrategia de gestión de respuestas más rica y flexible y extendemos las prueba de terminación incluyendo algunos casos de dominios de restricciones, como el dominio de Herbrand, que son compac constraint-compact. Después, aprovechando estas propiedades extendidas, diseñamos e implementamos un entorno genérico de TCLP, llamado Mod TCLP, que proporciona una interfaz clara y sencilla que facilita la integración de diferentes dominios de restricciones con el módulo de tabulación. Mod TCLP implementa de manera completa la comprobación mediante entailment de llamadas y respuestas mejorando el rendimiento y la terminación con respecto a Prolog, tabulación, CLP e implementaciones previas de TCLP. Validamos la expresividad y flexibilidad de Mod TCLP integrando diferentes resolutores de restricciones (uno de ellos escrito en C) y evaluamos su rendimiento con varios benchmarks. También usamos Mod TCLP para calcular agregados sobre retículos de manera incremental mediante un framework, ATCLP, que se basa en una nueva nueva semántica, y ve los agregados como restricciones y usa el entailment y la relación join del retículo para definir los agregados. Finalmente, aplicamos Mod TCLP para re-implementar el algoritmo de punto fijo de un intérprete abstracto de última generación donde el modulo de tabulación calcula el punto fijo y la interfaz de TCLP invoca el dominio abstracto para calcular el LUB de las sustituciones abstractas. El código resultante del intérprete abstracto es más simple y corto que el inicial y, en la mayoría de los casos, la implementación resultante es más rápida.

    Por otro lado, esta tesis extiende un razonador no monótono y goal-directed para evaluar programas CASP sin la fase de grounding requerida por la mayoría de los sistemas CASP. El razonador resultante, llamado s(CASP), calcula, a partir de una consulta, los modelos estables (parciales), que debido a la presencia de negación no estratificada en programas CASP podrían ser mas de uno, y el árbol de justificación con los términos y las reglas que soportan la consulta. Demostramos, mediante varios ejemplos, la mejora en la expresividad de s(CASP) con respecto a Prolog, ASP, CLP, y otros sistemas ASP con restricciones. Evaluamos brevemente la eficiencia de s(CASP) (que en algunos casos supera a un perfeccionado y altamente optimizado sistema ASP). A continuación, presentamos una aplicación real que se beneficia de la expresividad de s(CASP). Presentamos la implementación de un razonador automático que usa Event Caculus para modelar razonamiento de sentido común con una base lógica sólida. Intentos anteriores de automatizar el razonamiento utilizando la IA se enfrentaron a dificultades en el manejo de: cambios en dominios continuos y densos (por ejemplo, tiempo y cantidades físicas), restricciones entre variables, negación por defecto y una utilización homogénea de diferentes métodos de inferencia, entre otros. Mostramos cómo distintos escenarios de EC pueden ser modelados elegantemente usando el modelo de ejecución goal-directed de s(CASP) y cómo su expresividad permite realizar tareas de razonamiento deductivo en dominios que representan restricciones involucrando tiempo denso y fluentes con propiedades continuas.

    En conjunto, estos resultados arrojan ventajas en varios frentes: preguntas complejas y razonamiento no trivial son más fáciles de expresar gracias al mayor nivel de programación y restricciones lógicas; es necesaria una menor cantidad de cómputo gracias a la reutilización automática de datos inferencias previas (que, en cierto sentido, implementa automáticamente programación dinámicas); las consultas y las acciones asociadas (si las hubiere) pueden ser programadas usando el mismo formalismo. El uso de las herramientas resultantes, Mod TCLP y s(CASP), facilita la traducción de los requisitos del problema en código y minimiza la cantidad de reingeniería que es necesaria para adecuar los requisitos cuando estos cambian.