RA2013: Presentación del curso

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 y en los teoremas enormes (como el teorema de los 4 colores). Una colección de ejemplos de verificación se encuentra en el AFP.
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.
3. Leer los 10 primeros capítulos de los apuntes de programación funcional y los capítulos 2 y 8 de los apuntes de lógica informática.