ForMatUS: Eliminación de la implicación en Lean
En el vídeo, primero de la serie sobre conectivas lógicas, se comentan distintas demostraciones sobre la eliminación de la implicación en Lean. La primera es hacia atrás con tácticas y las siguientes son simplificaciones de la primera hasta llegar al término de la prueba. Finalmente, se presentan demostraciones automáticas.
Los enlaces correspondientes son: a la sesión en Lean Web, al código y al libro “DAO con Lean”.
A continuación, se muestra el vídeo