Diferencia entre revisiones de «Demostración Asistida por Ordenador con Coq»
De DAO con Coq
(Página creada con «Apuntes de demostración asistida por ordenador con [https://coq.inria.fr/ Coq] para los cursos de * [http://www.cs.us.es/~jalonso/cursos/m-ra/ Razonamiento automático] de…») |
|||
| Línea 9: | Línea 9: | ||
=== Temas === | === Temas === | ||
* [[Tema 1: Programación funcional y métodos elementales de demostración en Coq]]. | * [[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]]. | ||
Revisión del 14:58 31 jul 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.