LMF2013: Ejercicios de deducción natural en lógica proposicional con Isabelle/HOL (2)

En las clases del miércoles y de hoy del curso Lógica matemática y fundamentos se ha continuado comentando soluciones de los ejercicios de deducción natural en lógica proposicional con Isabelle/HOL de la relación 3.

También se han comentado ejercicios de la relación 4 (de argumentación proposicional con Isabelle/HOL) y de la relación 5 (de eliminación de conectivas).

Se ha propuesto la solución de los ejercicios de la relación 6 (sobre formalización de argumentos en lógica de primer orden).

Finalmente, se ha propuesto como tarea el enviar por correo la solución mediante deducción natural de 3 ejercicios elegidos entre los propuestos en los exámenes de los temas 2, 3 y 5 del libro de ejercicios.