RA2010: Razonamiento con cuantificadores, ecuacional y por casos en Isabelle
En la clase de hoy del curso de Razonamiento automático se ha visto cómo se puede escribir en Isabelle/Isar demostraciones de la lógica de primer orden, el razonamiento ecuacional y las demostraciones por casos.
En la clase se ha presentado el tema 2 (desde la página 21 a la 26) y el tema 3 (desde la página 26 a la 28)
El código correspondiente se encuentra en Cap_2.thy y Cap_3.thy–