LMF2018: Deducción natural proposicional con las tácticas Isabelle/HOL

En la clase de hoy del curso de Lógica matemática y fundamentos se ha estudiado cómo construir las pruebas por deducción natural usando las tácticas de Isabelle/HOL.

La teoría con los ejemplos presentados en la clase es la siguiente: