Lógicas modales con memoria

Desde la antigüedad hasta hoy, el campo de la lógica ha ido ganando fuerza y actualmente contribuye activamente en muchas áreas distintas, como filosofía, matemática, lingüística, ciencias de la computación, inteligencia artificial, fabricaci ón de hardware, etc. Cada uno de estos escenarios tiene necesidades espec íficas, que van desde requerimientos muy concretos, como un método de inferencia eficiente, hasta propiedades teóricas más abstractas, como un sistema axiomático elegante. Durante muchos años, los lenguajes clásicos (principalmente la lógica de primer orden) eran la alternativa a utilizar, pero esta gran variedad de aplicaciones hizo que otro tipo de lógicas empezaran a resultar atractivas en muchas situaciones. Supongamos que llega el momento de elegir una lógica para una tarea en particular. ¿Cómo podemos decidir cuál es la más adecuada? ¿Qué propiedades deberíamos buscar? ¿Cómo podemos "medir" una lógica con respecto a otras? Éstas no son preguntas sencillas, y no hay una receta general que uno pueda seguir. En esta tesis vamos a restringir estas cuestiones a una familia de lógicas en particular, y en ese contexto vamos a investigar algunos aspectos teóricos que nos van a ayudar a responder parte de estas inquietudes. Podemos aprender mucho estudiando casos particularmente interesantes, y nuestra contribución se va a desarrollar teniendo esa filosofía en mente. Las lógicas modales proposicionales ofrecen una alternativa a los lenguajes tradicionales. Pueden ser pensadas como un conjunto de herramientas que permiten diseñar lógicas específicamente construidas para una tarea en particular, posibilitando tener un control fino en su expresividad. Más aún, las lógicas modales resultaron tener un buen comportamiento computacional que probó ser bastante robusto frente a extensiones. Estas características, entre otras, ubicaron a las lógicas modales como una alternativa atractiva con respecto a los lenguajes clásicos. En este trabajo vamos a presentar una nueva familia de lógicas modales llamada memory logics. Las lógicas modales tradicionales posibilitan describir estructuras relacionales desde una perspectiva local, ¿pero cuál será el resultado si permitimos que una fórmula cambie la estructura en la que está siendo evaluada? Queremos explorar el efecto de agregar a las lógicas modales clásicas una estructura de almacenamiento explícita, una memoria, que permita modelar comportamiento dinámico a través de operadores que permitan almacenar y recuperar información de la memoria. Naturalmente, dependiendo del tipo de estructura de almacenamiento que utilicemos, y de qué operadores tengamos disponibles, la lógica resultante va a tener distintas propiedades que valen la pena investigar. Esta tesis está organizada de la siguiente manera. En el Capítulo 1 empezamos dando un breve resumen de cómo nacieron las lógicas modales, mostrando las diferentes perspectivas con las que históricamente se miró a la lógica modal. Luego presentamos formalmente a la lógica modal básica, y a un conjunto extendido de operadores que permiten apreciar el "estilo" modal de algunos lenguajes más ricos. Este capítulo ánaliza con un primer bosquejo de las memory logics, mostrando cómo pueden ayudar a modelar la noción de estado cuando dejamos a un conjunto como estructura de almacenamiento. El capítulo 2 está dedicado a presentar a las memory logics con detalle. En dicho capítulo mostramos algunos ejemplos que pueden ser descriptos agregando un conjunto a las estructuras relacionales estándar, junto con los operadores usuales sobre conjuntos que permiten agregar elementos y verificar pertenencia. A continuación mostramos otros operadores sobre conjuntos que pueden ser considerados, y discutimos la posibilidad de agregar restricciones a la interacción entre los operadores que trabajan sobre la memoria y los operadores modales. Estas restricciones pueden ser pensadas como una manera de lograr un control más úno en la expresividad. Dado que realizamos cambios en las lógicas modales clásicas, estamos interesados en analizar el impacto que esos cambios causaron en las lógicas resultantes. Por lo tanto, el resto del capítulo presenta un conjunto de herramientas a través de las cuales analizamos esta nueva familia de lógicas. Este conjunto de herramientas puede verse como un esquema que organiza el resto de la tesis, y que permite analizar a las memory logics en téerminos de expresividad, complejidad, interpolación y teoría de prueba. El resto de los capítulos investigan cada uno de estos aspectos en detalle. En los Capítulos 3 y 4 exploramos el poder expresivo de varias memory logics y estudiamos para cada fragmento la decidibilidad del problema de determinar la satisfactibilidad de una fórmula. En los casos decidibles, determinamos la complejidad computacional de cada uno. Analizamos el impacto de los diferentes operadores, su interacción, y también estudiamos otras estructuras de almacenamiento, como la pila. Luego, en el Capítulo 5, analizamos las propiedades de interpolación de Craig y definibilidad de Beth para algunas memory logics. También nos interesa estudiar a las memory logics desde la perspectiva de la teoría de prueba. En los Capítulos 6 y 7 nos volcamos al estudio de axiomatizaciones á la Hilbert y sistemas de tableau, y caracterizamos varios fragmentos usando principalmente técnicas utilizadas en lógicas híbridas. En el Capítulo 8 presentamos nuestras conclusiones, mencionamos algunos problemas abiertos y futuras direcciones de investigación