Introducción a la demostración asistida por ordenador con Isabelle/HOL
En el libro Introducción a la demostración asistida por ordenador con Isabelle/HOL he recopilado los temas y relaciones de ejercicios del curso de Razonamiento automático (2012-13).
El curso es una introducción a la demostración asistida por ordenador con Isabelle/HOL y consta de tres niveles.
En el primer nivel se presenta la formalización de las demostraciones por deducción natural. La presentación se basa en la realizada en los cursos de Lógica informática (de 2º del Grado en Informática) y Lógica matemática y fundamentos (de 3º del Grado en Matemáticas), en concreto en los temas de deducción natural proposicional y de primer orden. En este nivel se incluye los 3 primeros temas y las 6 primeras relaciones de ejercicios.
En el segundo nivel se presenta la programación funcional en Isabelle/HOL y el razonamiento sobre programas. La presentación se basa en la introducción a la programación con Haskell realizada en los cursos de Informática (de 1º del Grado en Matemáticas) y Programación declarativa (de 3º del Grado en Informática), en concreto en el tema 8 (para el razonamiento sobre programas) y en los restantes 9 primeros temas (para la programación funcional). En este nivel se incluye los temas 4, 5 y 6 y las relaciones de ejercicios desde la 7 a la 21.
En el tercer nivel se presentan casos de estudios y extensiones de la lógica para trabajar con conjuntos, relaciones y funciones. En este nivel se incluyen los temas 7 y 8 y las relaciones de ejercicios 22 y 23.
Tanto los temas como las relaciones de ejercicios se presentan como teorías de Isabelle/HOL (versión Isabelle2013). Conforme se necesitan se va comentando los elementos del Isabelle/HOL.
De Isabelle2013 se dispone se dispone de versiones libres para Linux, Windows y Mac OS X. Para instalarlo basta seguir la guía de instalación.