Diferencia entre revisiones de «Página principal»
De DAO con Coq
| Línea 3: | Línea 3: | ||
* [http://www.cs.us.es/~jalonso/cursos/lmf/ Lógica matemática y fundamentos] del [http://www.us.es/estudios/grados/plan_171?p=7 Grado en Matemáticas] de la [http://www.us.es Universidad de Sevilla]. | * [http://www.cs.us.es/~jalonso/cursos/lmf/ Lógica matemática y fundamentos] del [http://www.us.es/estudios/grados/plan_171?p=7 Grado en Matemáticas] de la [http://www.us.es Universidad de Sevilla]. | ||
| − | + | Esencialmente los apuntes son una adaptación del libro [https://softwarefoundations.cis.upenn.edu/current/lf-current 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 [http://www.glc.us.es/~jalonso/SLC2018 Seminario de Lógica Computacional]. | ||
| + | |||
| + | === 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]]. | ||
| + | * [[Tema 3: Datos estructurados en Coq]]. | ||
Revisión actual del 12:45 3 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.