RA2010: Panorama del razonamiento automático con Isabelle/HOL
La clase de hoy es la última del curso de Razonamiento automático. Se ha hecho una presentación de distintas aplicaciones que ayudan en el desarrollo de formalización del razonamiento con Isabelle/HOL y pequeños casos de estudi. Concretamente,
- formalización del algoritmo de Huffman,
- definición de un gramática como un conjunto inductivo y pruebas por inducción en dicho conjunto,
- trabajo con clases,
- trabajo con ámbitos,
- demostraciones estructuradas con Isar
- generación de código,
- automatización de demostraciones con Sledgehammer y
- búsqueda de contramodelo con Nitpick.
El código correspondiente se encuentra en Tema8.thy .