Autor: José A. Alonso

En la clase de hoy del curso Razonamiento automático se ha hecho una presentación del mismo, comentando los siguientes puntos

1. Objetivo: El objetivo fundamental del curso es la verificación de programas y de demostraciones matemáticas. Su necesidad se basa en la seguridad de sistemas críticos, en los teoremas incompletos y en los teoremas enormes (como el teorema de los 4 colores). Una colección de ejemplos de verificación se encuentra en The Archive of Formal Proofs.

2. Sistema: El sistema que se usará es Isabelle/HOL.

3. Punto de partida: El punto de partida es el conocimiento de la programación funcional con Haskell (correspondiente a los 10 primeros temas del curso de informática) y de la deducción natural (correspondiente a los temas 2 y 8 del curso de Lógica informática).

4. Metodología: El curso será esencialmente práctico con relaciones semanales de ejercicio. El material del curso se irá publicando en la página del curso, en la se pondrá los

   • temas (con las teorías de cada tema),
   • ejercicios (con los relaciones de ejercicios),
   • documentación (con enlaces a lecturas recomendadas),
   • sistemas (con enlaces a los sistemas utilizados) y
   • diario (con el resumen de cada clase).

Las dos referencias fundamentales son los apuntes Programming and proving in Isabelle/HOL y el libro A proof assistant for higher-order logic.

Como tareas para la próxima clase se propusieron:

1. Instalar Isabelle/HOL.
2. Leer alguna de las visiones generales del razonamiento automático.

Las clases del curso de Razonamiento automático del Máster Universitario en Lógica, Computación e Inteligencia Artificial comienzan el jueves 19 de octubre.

Las clases son los jueves de 16:30 a 18:30 en el Seminario del Departamento de Ciencias de la Computación e Inteligencia Artificial en el módulo E.

Las clases terminan el 8 de febrero de 2018.