I1M2018: Razonamiento sobre programas
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.