RA2010

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 .

En la clase de hoy del curso de Razonamiento automático se ha estudiado como caso de estudio, la formalización de un compilador de expresiones aritméticas y la demostración de su corrección en Isabelle. El contenido de la clase se encuentra en el tema 6 y el código correspondiente se encuentra en Cap_6.thy .

En la clase de hoy del curso de Razonamiento automático hemos comentados las soluciones de los ejercicios de la relación 1 (sobre deducción natural en lógica proposicional) y de la ewlación 2 (sobre deducción natural en lógica de primer orden) y hemos resueltos esjercicios de la relación 3 (sobre razonamiento por inducción sobre listas).

En la clase de hoy del curso de Razonamiento automático se han presentado los patrones fundamentales de demostración en Isabelle. En concreto, se han estudiado las demostraciones por casos, con negaciones, por contradicción, con equivalencias. También se ha estudiado la heurística de generalización en las demostraciones por inducción.

Las transparencias usadas en clase son las páginas 35-39 del tema 4 y las páginas 40-43 del tema 5.

El código correspondiente se encuentra en Cap_4.thy y Cap_5.thy.