RA2010: Patrones de demostración y heurística de generalización en Isabelle
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.