ForMatUS: Presentación de “DAO (Demostración Asistida por Ordenador) con Lean”
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
- Lógica matemática y fundamentos de 3º del Grado en Matemáticas.
- Lógica informática de 2º del Grado en Ingeniería Informática.
- Razonamiento automático del Máster Universitario en Lógica, Computación e Inteligencia Artificial.
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 primero, al código comentado,
- el segundo, a Lean Web con el ejercicio para experimentar en el navegador, y
- el tercero. a un vídeo explicando las soluciones del ejercicio.
El proyecto se desarrollará en
- el repositorio DAO_con_Lean de GitHub,
- el libro DAO (Demostración Asistida por Ordenador) con Lean
- los vídeos de la lista DAO (Demostración Asistida por Ordenador) con Lean de YouTube
- los mensajes en Twitter con la etiqueta #ForMatUS y
- las entradas en este blog con la categoría ForMatUS.
En el siguiente vídeo se presenta el proyecto: