Logica y Demostracion Automatica

En este curso vamos a dar una presentacion de distintas logicas (logica proposicional, logicas hibridas, logicas para la descripcion, logica de primer orden) y de distintos problemas de inferencia y metodos de solucion.

El curso consistira de clases teoricas y practicas. Durante las clases practicas se haran demos de demostradores para cada uno de los problemas de inferencia introducidos y se propondran tareas a resolver para obtener experiencia `hands-on.'

Miercoles: Logica Proposicional, Metodos Completos e Incompletos.
Introduciremos la Logica Proposicional (LP) y el problema SAT: dada una formula de LP decidir si existe una valuacion que la satisfaga. Analizaremos la complejidad del problema. Introduciremos el metodo de David-Putnam como metodo correcto y completo para SAT. Haremos una demo del demostrador zchaff. Introduciremos distintos metodos incompletos para SAT. Haremos una demo del demostrador walksat.
Jueves: Logicas Hibridas y Model Checking
Introduciremos la Logica Hibrida Basica y el problema de model checking: dada una formula y un modelo hibrido, decidir que elementos del dominio del modelo satisfacen la formula. Analizaremos la complejidad del problema. Daremos un algoritmo bottom-up para model checking del lenguaje hibrido. Haremos una demo del model checker mcheck.
Viernes: Description Logics y Tableaux
Introduciremos la Logica de Descripcion ALC y distintos problemas de inferencia estandard en logicas para la descripcion (subsumption, instance checking, etc). Analizaremos la complejidad de los distintos problemas. Introdiciremos el algoritmo de tableaux etiquetado para resolverlos. Haremos una demo del demostrador racer.
Sabado: Logica de Primer Orden y Resolucion
Introduciremos la Logica de Primer Orden (LPO) y el problema de SAT para LPO. Discutiremos la no computabilidad del problema. Introduciremos el metodo de resolucion como metodo correcto y completo para decidir satisfacibilidad de formulas de LPO. Haremos una demo del demostrador spass.

Slides

El material del curso esta linkeado mas abajo. Doy tambien versiones de los slides preparadas para imprimir (2x4 sin pausas), pero algunas animaciones funcionaran mal en esta presentacion. En el siguiente link se dan todos los handouts en un solo archivo.

El siguiente material se usara en las secciones practicas. Descargar el archivo .tgz con el software y el archivo .pdf con los ejercicios.

Bibliografia Adicional

Los siguientes articulos pueden resultar interesantes.

  • "Seventy-Five Problemas for Testing Automatic Theorem Provers", F. Pelletier, Journal of Automated Reasoning 2 (1986) 191--216.
    [pdf]
  • "The Search for Satisfaction", I. Gent and T. Walsh. Draft, 1999.
    [pdf]
  • "The SAT Phase Transition", I. Gent and T. Walsh, ECAI 94.
    [pdf]
  • "On the stupid algorithm for satisfiability", I. Gent, Technical report, APES-03-1998.
    [pdf]
  • "Common Syntax of the DFG-Schwerpunktprogramm `Deduktion'", R. Hahnle, M. Kerber, C. Weidenbach. Technical Report.
    [pdf]
  • "Resolution Strategies as Decision Procedures", W. Joyner, Journal of the ACM, Vol 23, No 3, 1976, 398--417.
    [pdf]
  • "Basic Description Logics", F. Baader and W. Nutt. Handbook of Description Logics.
    [pdf]
  • "Representation, Reasoning, and Relational Structures: a Hybrid Logic manifesto", P. Blackburn, Logic Journal of the IGPL, Vol 8, No 3, 2000, 339--365.
    [pdf]
  • "Model checking for hybrid logics (with an application to semistructured data)", M. Franceschet and M. de Rijke, Journal of Applied Logic, Vol 4, No 3, 2006, 279--304.
    [pdf]