Diferencia entre revisiones de «Demostración Asistida por Ordenador con Coq»
De DAO con Coq
| (No se muestran 3 ediciones intermedias del mismo usuario) | |||
| Línea 11: | Línea 11: | ||
* [[Tema 2: Demostraciones por inducción sobre los números naturales en Coq]]. | * [[Tema 2: Demostraciones por inducción sobre los números naturales en Coq]]. | ||
* [[Tema 3: Datos estructurados en Coq]]. | * [[Tema 3: Datos estructurados en Coq]]. | ||
| + | * [[Tema 4: Polimorfismo y funciones de orden superior en Coq]]. | ||
| + | * [[Tema 5: Tácticas básicas de Coq]]. | ||
| + | * [[Tema 6: Lógica en Coq]]. | ||
| + | |||
| + | === Código === | ||
| + | |||
| + | El código correspondiente se encuentra en [https://github.com/jaalonso/DAOconCoq GitHub]. | ||
| + | |||
| + | === Libro === | ||
| + | |||
| + | Todos los temas están recopilados en el libro [https://github.com/jaalonso/DAOconCoq/raw/master/texto/DAOconCoq.pdf Demostración asistida por ordenador con Coq]. | ||
Revisión actual del 12:41 20 ago 2018
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.
1 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.
- Tema 4: Polimorfismo y funciones de orden superior en Coq.
- Tema 5: Tácticas básicas de Coq.
- Tema 6: Lógica en Coq.
2 Código
El código correspondiente se encuentra en GitHub.
3 Libro
Todos los temas están recopilados en el libro Demostración asistida por ordenador con Coq.