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.

Esencialmente los apuntes son una adaptación del libro Software foundations (Vol. 1: Logical foundations) de Benjamin Peirce y otros.

Una primera versión de estos apuntes se han usado este año en el Seminario de Lógica Computacional.

Temas

• Tema 1: Programación funcional y métodos elementales de demostración en Coq.
• Tema 2: Demostraciones por inducción sobre los números naturales en Coq.
• Tema 3: Datos estructurados en Coq.