Ver el código de «Demostración Asistida por Ordenador con Coq»

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] del [http://master.cs.us.es/Máster_Universitario_en_Lógica,_Computación_e_Inteligencia_Artificial Máster Universitario en Lógica, computación e inteligencia artificial] 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 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]].

=== 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].