He añadido a la lista Lógica con Lean el vídeo Pruebas en Lean de P ∧ Q → Q ∧ P en el que se comentan 13 pruebas en Lean de la fórmula (P ∧ Q → Q ∧ P) en distintos estilos (declarativo, aplicativo con tácticas, funcional con término de prueba y automático).
Los enlaces correspondientes son:
A continuación, se muestra el vídeo
He añadido a la lista Lógica con Lean el vídeo Reglas de la conjunción en Lean en el que se e comentan 10 demostraciones en Lean que usan las reglas de introducción y eliminación de la conjunción en distintos estilos (declarativo, aplicativo con tácticas, funcional con término de prueba y automático).
Los enlaces correspondientes son:
A continuación, se muestra el vídeo
He añadido a la lista Lógica con Lean el vídeo Regla de introducción del condicional en Lean en el que se comentan 13 demostraciones en Lean de la regla de introducción del condicional en distintos estilos (declarativo, aplicativo con tácticas, funcional con término de prueba y automático). Además, se presenta el entorno de trabajo de Lean el de VS Code.
Los enlaces correspondientes son:
A continuación, se muestra el vídeo
He añadido a la lista Lógica con Lean el vídeo Regla de eliminación del condicional en Lean en el que se comentan 7 demostraciones en Lean de la regla de eliminación del condicional en distintos estilos (declarativo, aplicativo con tácticas, funcional con término de prueba y automático). Además,se presenta el entorno de trabajo de Lean en la Red (que permite hacer las pruebas en el navegador sin necesitar ninguna instalación).
Los enlaces correspondientes son:
A continuación, se muestra el vídeo
He añadido a la lista Lógica con Lean el vídeo Presentación de “Lógica con Lean” en el que se se comenta el proyecto de “Lógica con Lean”. Concretamente sus objetivos, bases y método de desarrollo.
Los enlaces correspondientes son:
A continuación, se muestra el vídeo