DAO con Coq DAO con Coq

Apuntes de demostración asistida por ordenador con Coq para los cursos de

• Razonamiento automático del Máster Universitario en Lógica, computación e inteligencia artificial de la Universidad de Sevilla.

• Lógica matemática y fundamentos del Grado en Matemáticas de la Universidad de Sevilla.

Temas

• [./Temas/T1_PF_en_Coq.html Tema 1]: Programación funcional y métodos elementales de demostración en Coq.