DAO con Coq DAOconCoq https://www.glc.us.es/~jalonso/DAOconCoq/index.php/Demostraci%C3%B3n_Asistida_por_Ordenador_con_Coq MediaWiki 1.31.14 first-letter Medio Especial Discusión Usuario Usuario discusión DAO con Coq DAO con Coq discusión Archivo Archivo discusión MediaWiki MediaWiki discusión Plantilla Plantilla discusión Ayuda Ayuda discusión Categoría Categoría discusión 0 13 70 65 2018-08-20T10:41:35Z Jalonso 1 wikitext text/x-wiki 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]. gwaj37f4cailkzb0pkhh3hlvgoei7gm