En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado cómo demostrar propiedades de programas Haskell.
Los tipos de razonamiento estudiado son
- Razonamiento ecuacional sin variables.
- Razonamiento ecuacional con variables.
- Razonamiento ecuacional con análisis de casos
- Razonamiento por inducción sobre los naturales
- Razonamiento por inducción sobre listas.
En las demostraciones por inducción se ha destacado la elección de variables, las demostraciones anidadas y la generalización de propiedades para su prueba por inducción.
Los apuntes correspondientes a la clase son los del tema 8
Además, se ha mostrado cómo automatizar las demostraciones usando Isabelle/HOL.