DAOconCoq: Demostración asistida por ordenador con Coq
Con esta nota inicio una serie sobre demostración asistida por ordenador con Coq.
Esencialmente las notas son una adaptación de Software foundations Vol. 1: Logical foundations para usarlas en los cursos de
- Razonamiento automático del Máster Universitario en Lógica, Computación e Inteligencia Artificial y
- Lógica matemática y fundamentos de 3º del Grado en Matemáticas.