Soluciones: Tarea 1
Durante la sesión de hoy veremos cómo se resolvían los ejercicios de la parte práctica de la tarea 1.
Para ello, realizamos primero los árboles de deducción natural de los teoremas dados, y luego escribimos el código de Haskell correspondiente.
Material
Durante la sesión utilicé un Notebook de Jupyter para escribir y compilar el contenido de Haskell.
Puedes descargar el notebook para ejecutarlo en tu propia instancia de iHaskell en el siguiente enlace: Sesion5.ipynb.
O puedes visualizar el material con los resultados ya ejecutados en: (Se publicará después de la clase)
Referencias
No se utilizaron referencias propias para esta sesión, pero podrían revisarse las referencias dadas durante la sesión sobre Ghost of Departed Proofs.
Además, pueden revisar la siguiente publicación con algunas proposiciones equivalentes a la regla de Tercero Excluido, junto con sus demostraciones, para caracterizar la Lógica Clásica: List of equivalents to Law of the Excluded Middle under intuitionistic logic.