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
En el vídeo se comentan distintas pruebas con Lean de una igualdad con productos de números reales. La primera es por reescritura usando las propiedades asociativa y conmutativa, La segunda es con encadenamiento de ecuaciones. 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 la transitividad de la igualdad de los números reales y cómo se trabaja con ellas en Lean Web. Las primeras son mediante reescritura y las últimas 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
Dentro del proyecto ForMatUS el primer subproyecto, titulado “DAO (Demostración Asistida por Ordenador) con Lean” tiene como base la lógica que se estudia en las asignaturas de
El objetivo concreto de este subproyecto es presentar una introducción a la DAO (Demostración Asistida con Ordenador) usando Lean para usarla en las clases de la asignatura de Razonamiento automático. Por tanto, el único prerrequisito es, como en el Máster, cierta madurez matemática como la que deben tener los alumnos de los Grados de Matemática y de Informática.
La exposición se hará mediante una colección de ejercicios. En cada ejercicios se mostrarán distintas pruebas del mismo resultado y se comentarán las tácticas conforme se van usando y los lemas utilizados en las demostraciones.
Además, para cada ejercicio se proporcionan tres enlaces:
El proyecto se desarrollará en
En el siguiente vídeo se presenta el proyecto: