Lógica Modal Computacional

Los Datos Más Imporantes

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 decision 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 Computacion como representación del conocimiento, model checking y verificacion formal de software y hardware.

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, HyLoRes, Bliksem), 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. Introduccion 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 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 logica 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. Unificacion. Resolucion para lógica de primer orden. Otras traducciones (funcional, ``layered''). 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 el site del curso en http://turing.wins.uva.nl/~carlos/LMC.

  • Areces and de Rijke, Computational Modal Logics (Libro en preparación)
  • Blackburn, de Rijke and Venema, Modal Logic, Capítulos 1, 2 y 6
  • Areces, Logic Engineering, Capítulos 1, 2 y 3
  • Goré, Tableau Methods for Modal and Temporal Logics
  • Tobies, Complexity Results and Practical Algorithms for Logics in Knowledge Representation, Capítulos 1, 2 y 3
  • 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.

Yo y Ms Circunstancias

Buenas, para aquellos que no me conocen, mi nombre es Carlos Areces. Me licencie en Ciencias de la Computación en la Universidad de Buenos Aires, para continuar mis estudios en la Universidad de Warwick, Inglaterra y en el Institute for Logic, Language and Computation (ILLC) de la Universidad de Amsterdam, Holanda, donde obtuve mi doctorado el a#o pasado. En la actualidad soy investigador del Computational and Applied Logic Group del ILLC.

Para "verme la cara" pueden visitar http://turing.wins.uva.nl/~carlos/, donde, ademas de charlas, papers, links a conferencias "and related academic stuff" pueden ver una foto mia. No confundir, el que está en primera plana, cruzado de brazos es Kermit, yo soy el que esta usando la remera con su foto.

El ILLC es uno de los centros de investigación en lógicas modales mas importantes. Recientemente su director, Prof. Johan van Benthem recibió el Premio Spinoza: un millón de dólares para investigación (esta es una demostración de que uno puede hacerse millonario haciendo lógica.) El principal interes del Computational and Applied Logic Group es el estudio de lenguages "a medida" para una determinada tarea de inferencia. En particular, nos interesa determinar exactamente el poder expresivo de diferentes lógicas, su facilidad de uso en diversas tareas de representación e inferencia, su complejidad teórica y la posibilidad de desarrollar algoritmos efectivos e implementables de deducción.

Pueden mandar cualquier pregunta, comentario, consejo espiritual, etc. a carlos@science.uva.nl. Nos vemos en el curso!!!!!