Demostración asistida por ordenador (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

• Tema 1: Programación funcional y métodos elementales de demostración en Coq.