Advanced Evaluation Techniques for (Non)-Monotonic Reasoning Using Rules with Constraints

Abstract

Constraint Logic Programming (CLP) is a declarative paradigm that extends Logic Programming (LP) with constraint solving capabilities over arbitrary domains that can be combined to model the problem to be solved. CLP brings additional expressive power to LP since constraints can very concisely capture complex relationships. That makes it easier to write programs that solve problems where no effective algorithm exists, and/or to adapt these programs when the problem specifications change. Additionally, the shift from “generate-and-test” to “constrain-and-generate” reduces the search tree and brings additional performance. CLP has been used in planning, scheduling, resource allocation, logistics, circuit design, and verification, among others. However, a CLP top-down execution strategy may enter loops in the presence of left recursion and/or non-stratified negation while a bottom-up execution strategy limits the range of admissible constraint domains, the places where constraints can appear, and the type (or number) of models that can be returned. This thesis contributes to the state of the art of Tabled Constraint Logic Programming (TCLP), which suspends subsumed calls checking entailment (improving termination properties of CLP programs), and of Constraint Answer Set Programming (CASP), which computes the stable model semantics of CLP programs with negation. First, we extend the theoretical foundation of TCLP by proving the soundness and completeness of a top-down operational semantics of TCLP that uses a richer and more flexible answer management strategy and we extend the proof of termination including arbitrary constraint domains (e.g., the Herbrand domain) even if they are not constraint-compact. Then, taking advantage of these extended properties we designed and implemented a generic TCLP framework, called Mod TCLP, provides a clear and simple interface that facilitates the integration of different constraint domains with a tabling engine. Mod TCLP fully implements the call and answer entailment check improving performance and termination w.r.t. Prolog, tabling, CLP, and previous TCLP implementations. We validated the expressiveness and flexibility of Mod TCLP integrating several constraint solvers (one of them written in C) and we evaluated its performance in several benchmarks. We also used Mod TCLP to incrementally compute lattice-based aggregates providing a framework, ATCLP, based on a new semantics that views the aggregates as constraints, and uses the entailment and join relations of the lattice to define the operations to compute and combine aggregates. Finally, we applied Mod TCLP to re-implement the fixpoint algorithm of a state-of-the-art abstract interpreter where the tabling engine computes the fixpoint and the TCLP interface invokes the abstract domain to compute the LUB of the abstract substitutions. The resulting code of the abstract interpreter is simpler and shorter than the initial one and, in most cases, the resulting implementation is faster. On the other hand, this thesis extends a goal-directed non-monotonic reasoner to compute CASP programs without the grounding phase required by most CASP systems. The resulting reasoner, called s(CASP), computes, given a query, the (partial) stable models, that due to the presence of non-stratified negation in CASP programs, could be more than one, and the justification tree with the terms and rules that support the query. We prove, through several examples, the enhanced expressiveness of s(CASP) system w.r.t. Prolog, ASP, CLP, and other ASP systems featuring constraints. We briefly discuss the efficiency of s(CASP) (which in some benchmarks outperforms a mature, highly optimized ASP system) and present a more complex application to exploit its expressiveness. Then, we present a real application that exploits the expressiveness of s(CASP). We present the implementation of an automated reasoner that uses Event Calculus to model commonsense reasoning with a sound, logical basis. Previous attempts to mechanize reasoning using EC faced difficulties in treating continuous change in dense domains (e.g., time and other physical quantities), constraints between variables, default negation, and the uniform application of different inference methods, among others. We show how EC scenarios can be elegantly modeled using the goaldirected execution model of s(CASP) and how its expressiveness makes it possible to perform deductive reasoning tasks in domains featuring constraints involving dense time and fluents with continuous properties. Together, these results envision advantages on several fronts: complex queries and nontrivial reasoning can be easier to express thanks to the higher-level of logic programming and constraints; fewer computations are needed thanks to the automatic reuse of previous inferences (which in some sense will automatically perform dynamic programming); queries and associated actions (if any) can be programmed using the same formalism. The use of the resulting tools, Mod TCLP and s(CASP), makes it easier translation of problem requirements into code and minimizes the amount of re-engineering needed to comply with the requirements when they change. ----------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 no son 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 módulo 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 más 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.