Los 400 últimos artículos de Vestigium son
- ForMatUS: Pruebas en Lean de ¬Q → ¬P ⊢ P → ¬¬Q
- ForMatUS: Pruebas en Lean de P → (Q → R), P, ¬R ⊢ ¬Q
- ForMatUS: Pruebas en Lean de la regla de introducción de la doble negación
- ForMatUS: Pruebas en Lean de P → Q ⊢ ¬Q → ¬P
- ForMatUS: Pruebas en Lean de P, P → Q, P → (Q → R) ⊢ R
- ForMatUS: Pruebas en Lean del modus tollens: P → Q, ¬Q ⊢ ¬P
- ForMatUS: Pruebas del silogismo hipotético: P → Q, Q → R ⊢ P → R
- ForMatUS: Pruebas en Lean de P → Q, P → ¬Q ⊢ ¬P
- ForMatUS: Reglas de la negación en Lean
- ForMatUS: Pruebas en Lean de P ∧ Q → Q ∧ P
- ForMatUS: Reglas de la conjunción en Lean
- ForMatUS: Regla de introducción del condicional en Lean
- ForMatUS: Regla de eliminación del condicional en Lean
- ForMatUS: Presentación de “Lógica con Lean”
- PFH: Definiciones de tipos en Haskell
- PFH: Funciones de orden superior en Haskell (Parte 2 de 3): Plegados
- PFH: Funciones de orden superior en Haskell (Parte 1 de 3)
- ForMatUS: El máximo común divisor de m y n es igual a m si, y sólo si, m divide a n (en Lean)
- ForMatUS: Formulación equivalente de lemas con dos hipótesis
- ForMatUS: Conmutatividad de la conjunción en Lean
- ForMatUS: Conectivas y desigualdades en Lean
- PFH: Definiciones por recursión en Haskell (Parte 2 de 2)
- PFH: Definiciones por recursión en Haskell (Parte 1 de 2)
- PFH: Cifrado César en Haskell
- ForMatUS: Monotonía de la multiplicación por no positivo (en Lean)
- ForMatUS: Monotonía de la multiplicación por no negativo (en Lean)
- ForMatUS: Suma de desigualdades (en Lean)
- ForMatUS: Suma de no negativos (en Lean)
- ForMatUS: La suma de no negativos es expansiva (en Lean)
- ForMatUS: Monotonía de la suma por la derecha en Lean
- ForMatUS: Monotonía de la suma por la izquierda en Lean
- ForMatUS: Eliminación de la disyunción en Lean
- ForMatUS: Introducción de la conjunción en Lean
- ForMatUS: Eliminación de la conjunción en Lean
- PFH: Definiciones por comprensión en Haskell
- ForMatUS: Eliminación de la equivalencia en Lean
- ForMatUS: Introducción de la implicación en Lean
- ForMatUS: Eliminación de la implicación en Lean
- PFH: Métodos elementales de definición de funciones en Haskell
- PFH: Tipos y clases en Haskell
- PFH: Introducción a la programación funcional con Haskell (Parte 2 de 2)
- PFH: Haskell con JupyterLab
- PFH: Introducción a la programación funcional con Haskell (Parte 1 de 2)
- ForMatUS: Ejercicios con Lean sobre aritmética real
- ForMatUS: Prueba en Lean con hipótesis y uso de lemas
- ForMatUS: Prueba en Lean mediante encadenamiento de ecuaciones
- ForMatUS: Prueba en Lean, mediante reescritura, de la transitividad de la igualdad
- ForMatUS: Presentación de “DAO (Demostración Asistida por Ordenador) con Lean”
- ForMatUS: Libro “Matemáticas en Lean”
- Proyecto ForMatUS (Formalización de las Matemáticas de la US)
- Resumen de lecturas compartidas durante julio de 2020
- Resumen de lecturas compartidas durante junio de 2020
- Resumen de lecturas compartidas durante mayo de 2020
- LMF2019: Definiciones inductivas en Isabelle/HOL
- I1M2019: El tipo abstracto de datos de grafos en Haskell
- I1M2019: El patrón de búsqueda en escalada en Haskell
- LMF2019: Desarrollo de teorías formalizadas con Isabelle/HOL
- I1M2019: El patrón de búsqueda por primero el mejor en Haskell
- Vídeos de las clases de razonamiento automático con Isabelle/HOL
- Vídeos de las clases de algorítmica con Haskell
- I1M2019: El patrón de búsqueda en espacios de estados en Haskell
- LMF2019: Razonamiento sobre árboles y bosques en Isabelle/HOL
- I1M2019: Resolución de problemas mediante búsqueda en espacios de estados
- I1M2019: El patrón de divide y vencerás en Haskell
- LMF2019: Razonamiento por casos y por inducción en Isabelle/HOL
- I1M2019: Programación dinámica en Haskell
- Resumen de lecturas compartidas durante abril de 2020
- I1M2019: El TAD de los polinomios en Haskell (2)
- LMF2019: Razonamiento sobre programas con Isabelle/HOL (2º parte)
- I1M2019: El TAD de los polinomios en Haskell
- I1M2019: El TAD de los montículos en Haskell
- I1M2019: El TAD de los árboles binarios de búsqueda en Haskell
- LMF2019: Razonamiento sobre programas con Isabelle/HOL (1º parte)
- I1M2019: Las librerías de conjuntos y de diccionarios en Haskell
- I1M2019: El TAD de los conjuntos en Haskell
- LMF2019: Programación funcional con Isabelle/HOL
- I1M2019: Algoritmos de ordenación en Haskell
- I1M2019: El tipo abstracto de datos de las colas de prioridad en Haskell
- Resumen de lecturas compartidas durante marzo de 2020
- I1M2019: El tipo abstracto de datos de las colas en Haskell
- I1M2019: El tipo abstracto de datos de las pilas en Haskell
- LMF2019: Deducción natural en lógica de primer orden (2/2)
- I1M2019: Análisis de la complejidad de los algoritmos
- I1M2019: Distancia esperada entre dos puntos de un cuadrado unitario
- LMF2019: Deducción natural en lógica de primer orden (1/2)
- I1M2019: Cálculo del número pi mediante el método de Montecarlo
- I1M2019: Aleatoriedad en Haskell
- Resumen de lecturas compartidas del 1 al 7 de marzo de 2020
- I1M2019: Combinatoria en Haskell
- LMF2019: Sintaxis y semántica de la lógica de primer orden
- I1M2019: Cálculo simbólico con Maxima
- LMF2019: Ejercicios de deducción natural con Isabelle/HOL (2)
- Resumen de lecturas compartidas durante febrero de 2020
- Reseña: Graph theory in Coq: minors, treewidth, and isomorphisms
- Resumen de lecturas compartidas del 22 al 29 de febrero de 2020
- LMF2019: Deducción natural proposicional (2)
- I1M2019: Introducción a la programación imperativa con Maxima
- I1M2019: Introducción al cálculo simbólico con Maxima
- LMF2019: Ejercicios de deducción natural con Isabelle/HOL (1)
- Reseña: Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi
- Resumen de lecturas compartidas del 16 al 21 de febrero de 2020
- I1M2019: Cálculo numérico en Haskell
- LMF2019: Deducción natural proposicional (1)
- I1M2019: Las librerías de vectores y matrices en Haskell
- LMF2019: Ejercicios de sintaxis y semántica de la lógica proposicional
- Reseña: Mac Lane’s comparison theorem for the Kleisli construction formalized in Coq
- Resumen de lecturas compartidas del 9 al 15 de febrero de 2020
- I1M2019: Ejercicios sobre vectores y matrices en Haskell
- RA2019: Verificación de la ordenación por inserción con Isabelle/HOL
- RA2019: Demostración en Isabelle de la corrección de un compilador
- LMF2019: Sintaxis y semántica de la lógica proposicional
- I1M2019: Matrices en Haskell
- LMF2019: Presentación del curso de “Lógica matemática y fundamentos”
- Resumen de lecturas compartidas del 1 al 8 de febrero de 2020
- Reseña: A comprehensive framework for saturation theorem proving
- LMF2019: Comienzo del curso
- RA2019: Reducción de SAT a Clique en Haskell
- RA2019: El algoritmo de Davis-Putnam en Haskell
- Resumen de lecturas compartidas durante enero de 2020
- Reseña: A formalised polynomial-time reduction from 3SAT to Clique
- Resumen de lecturas compartidas del 25 al 31 de enero de 2020
- RA2019: SAT (solving)
- Reseña: A formal proof of the irrationality of ζ(3)
- Resumen de lecturas compartidas del 19 al 24 de enero de 2020
- I1M2019: 3º examen de programación funcional con Haskell
- Reseña: The space of mathematical software systems
- Resumen de lecturas compartidas del 12 al 18 de enero de 2020
- RA2019: Deducción natural de primer orden con Isabelle/HOL
- Reseña: “Proof pearl: Braun trees”
- Resumen de lecturas compartidas del 1 al 11 de enero de 2020
- I1M2019: El juego de la vida en Haskell
- RA2019: Sintaxis y semántica de la lógica de primer orden
- I1M2019: Manejo de ficheros en Haskell
- I1M2019: Representación gráfica de funciones en Haskell con GNUplot
- I1M2019: Programas interactivos en Haskell
- Resumen de lecturas compartidas durante diciembre de 2019
- I1M2019: El problema de Hamming en Haskell
- I1M2019: El problema de las N reinas en Haskell
- I1M2019: Problema del concurso “Cifras y letras” en Haskell
- RA2019: Deducción natural proposicional con Isabelle/HOL (2)
- I1M2019: 2º examen de programación funcional con Haskell
- I1M2019: Ejercicios de evaluación perezosa y listas infinitas en Haskell
- RA2019: Deducción natural proposicional con Isabelle/HOL (1)
- I1M2019: Problemas de Exercitium del 22 y 29 de noviembre
- I1M2019: Evaluación perezosa en Haskell
- RA2019: Ejercicios de cuantificadores sobre listas en Isabelle/HOL
- RA2019: Razonamiento sobre árboles y bosques en Isabelle/HOL
- I1M2019: Problemas de Exercitium del 20 y 21 de noviembre
- I1M2019: Definiciones de clases en Haskell
- I1M2019: Programa en Haskell para reconocer tautologías
- Resumen de lecturas compartidas durante noviembre de 2019
- I1M2019: Introducción a la programación imperativa con Python
- I1M2019: Ejercicios sobre árboles binarios en Haskell
- RA2019: Ejercicios de razonamiento estructurado sobre programas en Isabelle/HOL
- RA2019: Razonamiento por casos y por inducción en Isabelle/HOL
- I1M2019: Problemas de Exercitium del 18 y 19 de noviembre
- I1M2019: De la matemática a la máquina
- I1M2019: Problemas de Exercitium del 14 y 15 de noviembre
- I1M2019: Definiciones de tipos en Haskell
- RA2019: Razonamiento estructurado sobre programas con Isabelle/HOL
- RA2019: Ejercicios de razonamiento sobre programas en Isabelle/HOL
- I1M2019: Problemas de Exercitium del 11 al 13 de noviembre
- I1M2019: Codificación binaria y transmisión de cadenas en Haskell
- RA2019: Razonamiento sobre programas con Isabelle/HOL (2/2)
- I1M2019: Ejercicios de funciones de orden superior
- I1M2019: El algoritmo de Luhn
- I1M2019: Funciones de orden superior en Haskell
- RA2019: Razonamiento sobre programas con Isabelle/HOL
- RA2019: Ejercicios de programación funcional en Isabelle/HOL
- I1M2019: Ejercicios auto-corregidos con Kattis
- Resumen de lecturas compartidas durante octubre de 2019
- RA2019: Programación funcional con Isabelle/HOL
- I1M2019: 1º examen de programación funcional con Haskell
- I1M2019: Operaciones conjuntistas con listas en Haskell
- I1M2019: Ejercicios de definiciones por recursión
- I1M2019: Ejercicios de definiciones por comprensión
- I1M2019: Definiciones por recursión (2)
- I1M2019: Definiciones por recursión (1)
- I1M2019: Programación de dibujos y listas por comprensión
- RA2019: Presentación del curso de “Razonamiento automático”
- RA2019: Comienzo del curso
- I1M2019: Ejercicios de definiciones con condicionales, guardas o patrones
- I1M2019: El cifrado César en Haskell
- I1M2019: Definiciones por comprensión
- I1M2019: Métodos elementales de definición de funciones en Haskell
- I1M2019: Tipos y clases en Haskell
- I1M2019: Ejercicios de definiciones por composición sobre números y listas (1)
- Resumen de lecturas compartidas durante septiembre de 2019
- I1M2019: Introducción a la programación funcional con Haskell
- I1M2019: Introducción a la programación funcional
- I1M2019: Comienzo del curso
- Resumen de lecturas compartidas durante el curso 2018-19
- Resumen de lecturas compartidas durante agosto de 2019
- Resumen de lecturas compartidas durante julio de 2019
- Resumen de lecturas compartidas durante junio de 2019
- I1M2018: Razonamiento sobre programas
- I1M2018: El problema del calendario mediante búsqueda en espacio de estado
- I1M2018: Programación dinámica: Apilamiento de barriles
- I1M2018: Algoritmos de ordenación en Haskell
- Resumen de lecturas compartidas durante mayo de 2019
- I1M2018: El problema de las fichas mediante búsqueda en espacio de estado
- I1M2018: Búsquedas heurísticas en Haskell
- LMF2018: Conjuntos, funciones y relaciones en Isabelle/HOL
- I1M2018: Resolución de problemas mediante búsqueda en espacios de estados
- I1M2018: El problema del granjero mediante búsqueda en espacio de estado.
- LMF2018: Desarrollo de teorías formalizadas con Isabelle/HOL
- I1M2018: El patrón de búsqueda en espacios de estados en Haskell
- I1M2018: Resolución de problemas mediante búsqueda en espacio de estados
- I1M2018: El rompecabeza del triominó mediante divide y vencerás
- I1M2018: El patrón de divide y vencerás en Haskell
- LMF2018: Definiciones inductivas en Isabelle/HOL
- LMF2018: Razonamiento sobre árboles y bosques en Isabelle/HOL
- I1M2018: Implementación en Haskell de algoritmos sobre grafos: recorridos, Kruskal y Prim
- I1M2018: El TAD (tipo abstracto de datos) de las tablas en Haskell
- LMF2018: Ejercicios de razonamiento sobre programas en Isabelle/HOL
- Resumen de lecturas compartidas durante abril de 2019
- I1M2018: Ejercicios con el TAD de grafos en Haskell
- I1M2018: Ejercicios sobre la implementación del TAD de grafos mediante listas
- I1M2018: El tipo abstracto de datos de grafos en Haskell
- I1M2018: El TAD de los multiconjuntos mediante diccionarios en Haskell
- I1M2018: División y factorización de polinomios mediante la regla de Ruffini en Haskell
- I1M2018: La librería de diccionarios en Haskell
- LMF2018: Programación funcional con Isabelle/HOL
- LMF2018: Primer examen de deducción natural con Isabelle/HOL
- I1M2018: Ejercicios con el tipo abstracto de dato de los montículos
- I1M2018: El TAD de los montículos en Haskell
- LMF2018: Ejercicios de deducción natural con las tácticas de Isabelle/HOL
- I1M2018: Relaciones binarias homogéneas con la librería de conjuntos de Haskell
- I1M2018: Operaciones con conjuntos con la librería Data.Set
- I1M2018: La librería de conjuntos en Haskell
- LMF2018: Deducción natural en lógica de primer orden con las tácticas Isabelle/HOL
- Resumen de lecturas compartidas durante marzo de 2019
- I1M2018: Ejercicios con el tipo de dato de los conjuntos en Haskell
- I1M2018: El TAD de los conjuntos en Haskell
- LMF2018: Ejercicios de deducción natural de lógica proposicional con las tácticas de Isabelle/HOL
- LMF2018: Ejercicios de deducción natural en lógica de primer orden con Isabelle/HOL (2)
- I1M2018: Resolución de una ecuación con factoriales en Haskell
- I1M2018: Ejercicios con el tipo abstracto de dato de las colas
- I1M2018: El tipo abstracto de datos de las colas de prioridad en Haskell
- LMF2018: Deducción natural proposicional con las tácticas Isabelle/HOL
- I1M2018: Ejercicios con el tipo abstracto de dato de las pilas
- I1M2018: El tipo abstracto de datos de las colas en Haskell
- LMF2018: Ejercicios de deducción natural en lógica de primer orden con Isabelle/HOL
- LMF2018: Deducción natural en lógica de primer orden
- I1M2018: El tipo abstracto de datos de las pilas en Haskell
- I1M2018: De la matemática a la máquina
- I1M2018: Análisis de la complejidad de los algoritmos
- LMF2018: Ejercicios de sintaxis y semántica de la lógica de primer orden
- I1M2018: 4º examen de programación funcional con Haskell
- LMF2018: Sintaxis y semántica de la lógica de primer orden
- I1M2018: Ejercicios de estadística descriptiva con las librerías de Haskell
- I1M2018: Estadística descriptiva en Haskell
- LMF2018: Ejercicios de deducción natural con Isabelle/HOL (1)
- I1M2018: Ejercicios de programación de cálculo numérico en Maxima
- I1M2018: Cálculo numérico en Haskell (2º parte)
- I1M2018: Programación dinámica: Caminos en una retícula
- I1M2018: Ejercicios de programación dinámica
- LMF2018: Deducción natural proposicional con Isabelle/HOL
- Resumen de lecturas compartidas durante febrero de 2019
- I1M2018: Cálculo numérico en Haskell
- I1M2018: Introducción a la programación imperativa con Maxima y Python
- LMF2018: Deducción natural proposicional (2)
- I1M2018: Cálculo simbólico con Maxima
- LMF2018: Ejercicios de deducción natural con Pandora
- LMF2018: Ejercicios de sintaxis y semántica de la lógica proposicional
- I1M2018: Programación dinámica en Haskell
- LMF2018: Deducción natural proposicional (1)
- LMF2018: Sintaxis y semántica de la lógica proposicional (2)
- I1M2018: Las librerías de vectores y matrices en Haskell
- I1M2018: Ejercicios sobre vectores y matrices en Haskell
- LMF2018: Sintaxis y semántica de la lógica proposicional
- RA2018: Razonamiento automático con Coq
- I1M2018: Matrices en Haskell
- LMF2018: Presentación del curso de “Lógica matemática y fundamentos”
- RA2018: Conjuntos, funciones y relaciones en Isabelle/HOL
- RA2018: Definiciones inductivas en IsabelleHOL
- LMF2018: Comienzo del curso
- Resumen de lecturas compartidas durante enero de 2019
- RA2018: Demostración en Isabelle de la corrección de un compilador
- RA2018: Deducción natural de primer orden con Isabelle/HOL
- RA2018: Sintaxis y semántica de la lógica de primer orden
- RA2018: Editores lógicos
- I1M2018: 3º examen de programación funcional con Haskell
- I1M2018: 3º concurso de programación en Kattis
- RA2018: Deducción natural proposicional con Isabelle/HOL
- I1M2018: 2º concurso de programación en Kattis
- I1M2018: Resolución de problemas en Kattis
- I1M2018: Manejo de ficheros en Haskell
- I1M2018: Representación gráfica de funciones en Haskell con GNUplot
- I1M2018: Programas interactivos en Haskell
- Resumen de lecturas compartidas durante diciembre de 2018
- I1M2018: El problema de Hamming en Haskell
- I1M2018: El problema de las N reinas en Haskell
- I1M2018: Problema del concurso “Cifras y letras” en Haskell
- RA2018: Verificación de algoritmos de ordenación con Isabelle/HOL
- I1M2018: 2º examen de programación funcional con Haskell
- I1M2018: Ejercicios de evaluación perezosa y listas infinitas en Haskell
- RA2018: Razonamiento sobre árboles y bosques en Isabelle/HOL
- I1M2018: Evaluación perezosa en Haskell
- I1M2018: Definiciones de clases en Haskell
- I1M2018: Ejercicios de tipos de datos algebraicos en Haskell
- Resumen de lecturas compartidas durante noviembre de 2018
- I1M2018: Ejercicios sobre árboles binarios en Haskell
- RA2018: Razonamiento por casos y por inducción en Isabelle/HOL
- I1M2018: Programa en Haskell para reconocer tautologías
- I1M2018: Ejercicios de funciones de orden superior
- I1M2018: Definiciones de tipos en Haskell
- RA2018: Razonamiento estructurado sobre programas con Isabelle/HOL
- I1M2018: Ejercicios sobre cadenas en Haskell
- I1M2018: Codificación binaria y transmisión de cadenas en Haskell
- RA2018: Razonamiento automático sobre programas en Isabelle/HOL
- I1M2018: Funciones de orden superior en Haskell
- I1M2018: Operaciones conjuntistas con listas en Haskell
- I1M2018: El cifrado César en Haskell
- RA2018: Programación funcional con Isabelle/HOL
- GAMPUS2018: 3ª sesión (7-nov-18)
- I1M2018: 1º examen de programación funcional con Haskell
- Resumen de lecturas compartidas durante octubre de 2018
- I1M2018: Ejercicios de definiciones por recursión
- I1M2018: Ejercicios de definiciones por comprensión (3)
- I1M2018: Ejercicios de autoevaluación
- Presentación del Seminario de Algorítmica, Matemáticas y Programación
- I1M2018: Ejercicios de definiciones por comprensión (2)
- RA2018: Presentación del curso de “Razonamiento automático”
- RA2018: Comienzo del curso
- I1M2018: Ejercicios de definiciones por comprensión (1)
- I1M2018: Ejercicios de definiciones con condicionales, guardas o patrones (2)
- I1M2018: Definiciones por recursión
- I1M2018: Ejercicios de definiciones con condicionales, guardas o patrones (1)
- I1M2018: Ejercicios de definiciones por composición sobre números y listas (3)
- I1M2018: Programación de dibujos y listas por comprensión
- I1M2018: Ejercicios de definiciones por composición sobre números y listas (2)
- I1M2018: Definiciones por comprensión
- I1M2018: Métodos elementales de definición de funciones en Haskell
- I1M2018: Tipos y clases en Haskell
- I1M2018: Ejercicios de definiciones por composición sobre números y listas (1)
- Resumen de lecturas compartidas durante septiembre de 2018
- I1M2018: Introducción a la programación funcional con Haskell
- I1M2018: Introducción a la programación funcional
- Reseña: Proving tree algorithms for succinct data structures
- Reseña: Formal verification of a geometry algorithm (A quest for abstract views and symmetry in Coq proofs)
- Reseña: “Concrete semantics” with Coq and CoqHammer
- I1M2018: Comienzo del curso
- Hammer for Coq (automation for dependent type theory)
- Reseña: Comparison of two theorem provers: Isabelle/HOL and Coq
- Reseña: A formal proof of the computation of Hermite normal form in a general setting
- Resumen de lecturas compartidas durante agosto de 2018
- Resumen de lecturas compartidas durante julio de 2018
- Programación funcional y métodos elementales de demostración en Coq
- DAOconCoq: Demostración asistida por ordenador con Coq
- Resumen de lecturas compartidas durante el curso 2017-18
- Resumen de lecturas compartidas durante junio de 2018
- Resumen de lecturas compartidas durante mayo de 2018
- Resumen de lecturas compartidas durante abril de 2018
- I1M2017: Ejercicios con el TAD de los polinomios en Haskell
- I1M2017: Relaciones binarias homogéneas con la librería de conjuntos de Haskell
- LMF2017: Ejercicios de lógica de primer orden
- I1M2017: Ejercicios con el tipo abstracto de dato de las pilas
- I1M2017: Haskell para ciencias del dato
- I1M2017: Emacs para ciencias del dato
- LMF2017: Tableros semánticos.
- I1M2017: El TAD de los polinomios en Haskell
- LMF2017: Deducción natural de primer orden con Isabelle/HOL
- I1M2017: Las librerías de conjuntos y de diccionarios en Haskell
- I1M2017: El TAD de los conjuntos en Haskell
- LMF2017: Deducción natural en lógica de primer orden
- Resumen de lecturas compartidas durante marzo de 2018
- I1M2017: Escritura de documentos, LaTeX, PDF y HTML con el modo Org de Emacs
- LMF2017: Ejercicios de sintaxis y semántica de la lógica de primer orden
- LMF2017: Ejercicios de deducción natural proposicional en Isabelle/HOL (2)
- SLC2018: Datos estructurados en Coq
- I1M2017: Programación dinámica: Apilamiento de barriles
- I1M2017: Programación dinámica: Caminos en una retícula
- I1M2017: El tipo abstracto de datos de las colas de prioridad en Haskell
- LMF2017: Semántica de la lógica de primer orden
- I1M2017: El tipo abstracto de datos de las colas en Haskell
- I1M2017: El tipo abstracto de datos de las pilas en Haskell
- LMF2017: Ejercicios de deducción natural proposicional en Isabelle/HOL
- SLC2018: Demostraciones por inducción en Coq
- I1M2017: 4º examen de programación funcional con Haskell
- LMF2017: Sintaxis y semántica de la lógica de primer orden
- LMF2017: Representación del conocimiento mediante lógica de primer orden
- I1M2017: Programación dinámica en Haskell
- I1M2017: Ejercicios de programación de cálculo numérico en Maxima
- I1M2017: Cálculo numérico en Haskell (2º parte)
- I1M2017: Análisis de la complejidad de los algoritmos
- LMF2017: Deducción natural proposicional con Isabelle/HOL
- I1M2017: De la matemática a la máquina
- I1M2017: Introducción a la programación con Maxima
- SLC2018: Programación funcional en Coq
- LMF2017: Ejercicios de deducción natural proposicional
- Resumen de lecturas compartidas (febrero de 2018)
- LMF2017: Deducción natural proposicional (2)
- I1M2017: Cálculo simbólico con Maxima
- I1M2017: Cálculo numérico en Haskell
- LMF2017: Deducción natural proposicional (1)
- SLC2018: Presentación del “Seminario de Lógica Computacional” (2018)
- I1M2017: Combinatoria en Haskell
- LMF2017: Consecuencia lógica y demostrabilidad
- I1M2017: Ejercicios de estadística descriptiva con las librerías de Haskell