RA2018: Presentación del curso de “Razonamiento automático”

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: Los sistemas que se usarán son Isabelle/HOL y Coq.

  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, para la parte de Isabelle/HOL, 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: