Lógica Modal Computacional
Información General

Introducción

Las Lógicas Modales desde una Perspectiva Actual

En su perspective más moderna, las lógicas modales son vistas como herramientas para indentificar fragmentos interesantes de lógicas de primer y alto orden, para una determinada tarea de modelaje o inferencia.

``Interesante'' usualmente significa: de baja complejidad, buenas propiedades metalógicas (completitud, interpolación, etc.), poder expresivo adecuado, simple diseño de algoritmos de decisión y de herramientas automáticas de inferencia, simplicidad de uso, etc.

Por el otro lado, las posibles ``tareas de modelaje o inferencia'' pueden ser extremandamente variadas, desde aplicaciones clásicas en filosofía y epistemología, usos en linguística (el trabajo fundacional de Prior en Tense Logic y el análisis de tiempos verbales, o el trabajo más reciente en Multimodal Categorial Logics ), a los usos más proximos a la Ciencia de la Computación como representación del conocimiento, model checking y verificación formal de software y hardware.

Aquellos que quieran saber un poco más sobre esta perspectiva ``ingenieril'' de las lógicas modales, pueden darle una mirada a los slides de la charla ``Lógicas Computacionales a Medida.''

El Curso

El principal énfasis teórico del curso será en los aspectos computacionales de lenguages modales (incluyendo lenguajes modales no standard, como lógicas híbridas y lógicas para descripción). En particular, discutiremos diferentes métodos de inferencia y decisión (directos e indirectos), su complejidad y posibles heurísticas y optimizaciones para problemas de satisfiabilidad.

En las clases prácticas presentaremos una selección de herramientas para deducción automática (RACER, Bliksem, HyLoRes), complementando las nociones teóricas con experiencia de laboratorio.

El curso no requiere conocimientos previos de lógica modal, pero sí asume conocimientos básicos sobre lógica proposicional y de predicados.

La siguiente es una lista tentativa de temas, en el orden en que serían presentados en el curso. Si alguien está interesado en algún otro tema relacionado con lógicas modales computacionales, se puede poner en contacto conmigo (carlos@science.uva.nl) e intentaré incluirlo en el curso.

• Semana 1: Ventajas y desventajas de las lógicas clásicas. Introducción a la lógica modal. Lógicas modales como fragmentos de lógicas clásicas. Poder expresivo. Nociones de básicas de bisimulación. Métodos de decisión y su complejidad. Un menú de lógicas modales. Ejemplos de applicación.
• Semana 2: El método de tableux. Tableux clásicos. Correctitud, completitud y terminación. Lógicas para la descripción. Bases de conocimiento. Nociones de consecuencia global y local. Inferencia a partir de bases de conocimiento (T- and A-Box reasoning). Prefixed tableaux. Complejidad PSPACE de K. Logicas en EXPTIME. Heuristicas y optimizaciones: catching, backjumping, etc. El demostrador automático RACER.
• Semana 3: La traducción standard. Caracterización del fragmento modal de lógica de primer orden. Otros fragmentos modales de la lógica de primer (y segundo) orden. Satisfiabilidad modal como satisfiabilidad de primer orden. Ventajas y desventajas del mapeo dentro de primer orden. El método de resolución. Resolución para lógica proposicional. Unificación. Resolución para lógica de primer orden. Otras traducciones (funcional, layered, etc). Comparación. El demostrador automático Bliksem.
• Semana 4: Lógicas híbridas. Referencia explícita a elementos del modelo. Poder expresivo y complejidad. Ejemplos de modelado usando lógicas híbridas. Lógicas para la descripción desde el punto de vista de las lógicas híbridas. Internalización de tableaux. Resolución directa clásica de lógicas modales. Resolución en lógicas híbridas. El demostrador automático HyLoRes (with all the nitty-gritty details :)).

Bibliografía Básica: Toda la bibliografia relevante va a ser puesta a disposición en estas páginas.

• Areces and de Rijke, Computational Modal Logics (Libro en preparación)
• Blackburn, de Rijke and Venema, Modal Logic, Capítulos 1, 2 y 6. Guía a la Literatura. La bibliografía
• Areces, Logic Engineering, Capítulos 1 y 2. La bibliografía
• Goré, Tableau Methods for Modal and Temporal Logics (correcciones)
• Tobies, Complexity Results and Practical Algorithms for Logics in Knowledge Representation, Capítulos 1, 2 y 3. La bibliografía
• Horrocks and Patel-Schneider, Optimising Description Logic Subsumption
• de Nivelle, Schmidt, and Hustadt, Resolution-Based Methods for Modal Logics
• Areces, Monz, de Nivelle and de Rijke, The Guarded Fragment: Ins and Outs
• Areces, Gennari, Heguiabehere and de Rijke, Tree-Based Heuristics in Modal Theorem Proving
• Blackburn, Representation, Reasoning, and Relational Structures: a Hybrid Logic Manifesto
• Blackburn, Internalizing Labelled Deduction
• Areces, de Nivelle and de Rijke, Resolution in Modal, Description and Hybrid Logic

Horario

El curso se dictará durante las cuatro semanas de Setiembre, con dos clases teóricas por semana de tres horas cada una, más una clase práctica (ejercicios/laboratorio) de dos horas, para sumar un gran total de 8 horas semanales de lógica modal.

Los horarios definitivos y el aula donde se dictarán las clases serán anunciados pronto.

Como ven, el curso va a ser realmente intensivo. A cambio de esta dosis masiva de lógica modal, los alumnos que pasen la evaluación final (detalles mas abajo), recibirán dos puntos de materias optativas.

Además, durante el curso se presentará un buen número de temas aptos para tesis de licenciatura. Aquellos que estén interesados podrán discutirlos conmigo y coordinar colaboraciones con gente en Amsterdam.

Evaluación

Durante las clases teóricas se indicarán ejercicios (teóricos y prácticos), algunos de los cuales serán seleccionados como parte de la evaluación final.

Un archivo conteniendo el enunciado definitivo de los ejercicios elegidos para la evaluacion final con su valor en puntos será accessible desde este link.

Los ejercicios pueden ser discutidos conmigo durante el curso. Durante las clases prácticas resolveremos ejercicios similares a los de la evaluación.

Luego de terminado el curso, aquellos que quieran aprobar y obtener una nota final, deberán enviarme dentro del siguiente mes respuestas a los ejercicios para su corrección. La elección de que ejercicios resolver es libre. Para la aprobación del curso, se deben obtener al menos 40 puntos en ejercicios teóricos y 40 puntos en ejercicios prácticos.