ForMatUS

En el vídeo se comentan distintas demostraciones sobre la eliminación de la equivalencia en Lean. La primera es con la táctica intro y las siguientes son simplificaciones de la primera hasta llegar al término de la prueba. A continuación, se presentan demostraciones estructuradas con razonamiento hacia adelante y, 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

En el vídeo se comentan distintas demostraciones sobre la introducción de la implicación en Lean. La primera es con la táctica intro 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

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

En el vídeo se comentan distintas pruebas con Lean de ejercicios sobre la aritmética de los números reales. La primera es por reescritura, la segunda es con encadenamiento de ecuaciones y las restantes son 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

En el vídeo se comentan distintas pruebas con Lean de una propiedad de la aritmética de los números reales con hipótesis. La primera es por reescritura y la segunda es con encadenamiento de ecuaciones. Las restantes son automáticas.

El enlace a la sesión es

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