RA2010: Razonamiento proposicional con 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 proposicional.
En la clase se ha presentado desde la página 15 a la 21 de los apuntes
GDE Error: Error al recuperar el fichero. Si es necesario, desactiva la comprobación de errores (404:Not Found)
El código correspondiente se encuentra en Cap_2.thy.