RA2010: Ejercicios de razonamiento proposicional con Isabelle
La clase de hoy del curso de Razonamiento automático ha consistido en la formalización en Isabelle/Isar de demostraciones por deducción natural en lógica proposicional. Para ello se han formalizado todas las demostraciones del tema de deducción natural proposicional del curso de Lógica informática
Las formalizaciones realizadas en clase se encuentran en el siguiente documento
GDE Error: Error al recuperar el fichero. Si es necesario, desactiva la comprobación de errores (404:Not Found)
Se ha dejado como tarea para la próxima clase la formalización de las demostraiones del resto del tema y la solución de los ejercicios de la 1ª relación.