Los 400 últimos artículos de Vestigium son
- Resumen de lecturas compartidas durante agosto de 2021
- Resumen de lecturas compartidas durante julio de 2021
- Resumen de lecturas compartidas durante junio de 2021
- Resumen de lecturas compartidas durante mayo de 2021
- Resumen de lecturas compartidas durante abril de 2021
- Resumen de lecturas compartidas durante marzo de 2021
- Resumen de lecturas compartidas durante febrero de 2021
- Resumen de lecturas compartidas durante enero de 2021
- Pruebas en Lean de “La función identidad no está acotada superiormente”
- Negación del universal en Lean: Caracterización de funciones no pares
- Negación del existencial en Lean: Caracterización de números no pares
- Pruebas en Lean de la ley de De Morgan: ¬(P ∧ Q) ↔ ¬P ∨ ¬Q
- Pruebas en Lean de “Un número es par si, y sólo si, lo es su cuadrado”
- Pruebas en Lean de “La relación menor es irreflexiva en los reales”
- Pruebas en Lean de “Si u es una sucesión de Cauchy y a es un punto de acumulación de u, entonces a es el límite de u”
- Pruebas en Lean de “Toda sucesión convergente es una sucesión de Cauchy”
- ForMatUS: Pruebas en Lean de “El punto de acumulación de las convergentes es su límite”
- ForMatUS: Pruebas en Lean de “Las subsucesiones tienen el mismo límite que la sucesión”
- ForMatUS: Pruebas en Lean de “Hay infinitos términos arbitrariamente próximos a los puntos de acumulación”
- ForMatUS: Pruebas en Lean de “Las funciones de extracción no están acotadas”
- ForMatUS: Pruebas en Lean de “La función identidad es menor o igual que la función de extracción”
- ForMatUS: Pruebas en Lean de “Los supremos de las sucesiones no decrecientes son sus límites”
- ForMatUS: Pruebas en Lean de la unicidad del límite de las sucesiones
- Pruebas en Lean de “Si |x – y| ≤ ε, para todo ε > 0, entonces x = y”
- ForMatUS: Si |x| < ε, para todo ε > 0, entonces x = 0
- ForMatUS: Pruebas en Lean del teorema del emparedado
- Resumen de lecturas compartidas durante diciembre de 2020
- Resumen de lecturas compartidas durante noviembre de 2020
- ForMatUS: Pruebas en Lean de propiedades de la composición de funciones (elemento neutro y asociatividad)
- ForMatUS: Pruebas en Lean de que la identidad es biyectiva
- ForMatUS: Pruebas en Lean de que las relaciones reflexivas y euclídeas son de equivalencia
- ForMatUS: Pruebas en Lean de que las equivalencias son los preórdenes simétricos
- Resumen de lecturas compartidas durante octubre de 2020
- ForMatUS: Pruebas en Lean de una desigualdad entre números naturales
- ForMatUS: Pruebas en Lean de que las partes simétricas son simétricas
- ForMatUS: Pruebas en Lean de que las partes simétricas de las relaciones reflexivas son reflexivas
- ForMatUS: Pruebas en Lean de que las partes estrictas de los órdenes parciales son transitivas
- ForMatUS: Pruebas en Lean de que las partes estrictas son irreflexivas
- ForMatUS: Pruebas en Lean de que las relaciones irreflexivas y transitivas son asimétricas
- ForMatUS: Pruebas en Lean de 𝒫 A ⊆ 𝒫 B ↔ A ⊆ B
- ForMatUS: Pruebas en Lean de (⋃i, ⋂j, A i j) ⊆ (⋂j, ⋃i, A i j)
- ForMatUS: Pruebas en Lean de la intersección sobre unión general: C ∩ (⋃i, A i) = (⋃ i, C ∩ A i)
- ForMatUS: Pruebas en Lean de la distributiva de la intersección general sobre la intersección
- ForMatUS: Pertenencia a uniones e intersecciones de familias en Lean
- ForMatUS: Unión e intersección de familias de conjuntos en Lean
- ForMatUS: Pruebas en Lean de (A ∩ Bᶜ) ∪ B = A ∪ B
- PFH: Sistema de decisión de tautologías en Haskell
- ForMatUS: Pruebas en Lean de la propiedad distributiva de la intersección sobre la unión
- ForMatUS: Pruebas en Lean de la conmutatividad de la intersección
- ForMatUS: Complementario de un conjunto en Lean (Pruebas de A \ B ⊆ Bᶜ)
- ForMatUS: Diferencia de conjuntos en Lean (Pruebas de A \ B ⊆ A)
- ForMatUS: Regla del conjunto vacío en Lean
- ForMatUS: Regla de introducción de la unión en Lean
- ForMatUS: Regla de introducción de la intersección en Lean
- ForMatUS: Pruebas en Lean de la antisimetría de la inclusión de conjuntos
- ForMatUS: Pruebas en Lean de la reflexividad de la inclusión de conjuntos
- ForMatUS: Pruebas en Lean del desarrollo de un producto de dos sumas
- ForMatUS: Pruebas en Lean de (x + y) + z = (x + z) + y
- ForMatUS: Pruebas en Lean de y = x → y = z → x = z
- ForMatUS: Pruebas en Lean de la transitividad de la igualdad
- ForMatUS: Regla de eliminación de la igualdad en Lean
- ForMatUS: Pruebas en Lean de ∃x∃y P(x,y) ↔ ∃y∃x P(x,y)
- ForMatUS: Pruebas en Lean de ∃x (P(x) ∨ Q(x)) ↔ ∃x P(x) ∨ ∃x Q(x)
- ForMatUS: Pruebas en Lean de ∀x (P(x) ∧ Q(x)) ↔ ∀x P(x) ∧ ∀x Q(x)
- ForMatUS: Pruebas en Lean de ¬∀x P(x) ↔ ∃x ¬P(x)
- ForMatUS: Regla de eliminación del cuantificador existencial en Lean
- ForMatUS: Regla de introducción del cuantificador existencial en Lean
- Resumen de lecturas compartidas durante septiembre de 2020
- ForMatUS: Regla de introducción del cuantificador universal en Lean
- ForMatUS: Regla de eliminación del cuantificador universal en Lean
- ForMatUS: Pruebas en Lean de ¬P → Q, ¬Q ⊢ P
- ForMatUS: Pruebas en Lean de P, ¬¬(Q ∧ R) ⊢ ¬¬P ∧ R
- ForMatUS: Pruebas en Lean de P → Q ⊢ ¬P ∨ Q
- ForMatUS: Pruebas en Lean del principio del tercio excluso
- ForMatUS: Pruebas en Lean de la eliminación de la doble negación
- ForMatUS: Pruebas en Lean de la regla de reducción al absurdo
- PFH: Programas, funciones y dibujos (Introducción a la programación funcional con CodeWorld/Haskell)
- ForMatUS: Reglas de eliminación del bicondicional en P ↔ Q, P ∨ Q ⊢ P ∧ Q
- ForMatUS: Pruebas en Lean de P ∧ Q ↔ Q ∧ P
- ForMatUS: Pruebas en Lean de ¬P ∨ Q ⊢ P → Q
- ForMatUS: Pruebas en Lean de P → (Q → P)
- ForMatUS: Pruebas de Q → R ⊢ P ∨ Q → P ∨ R
- ForMatUS: Pruebas en Lean de P ∨ Q ⊢ Q ∨ P
- ForMatUS: Regla de eliminación de la disyunción en Lean
- ForMatUS: Reglas de introducción de la disyunción en Lean
- 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
- Resumen de lecturas compartidas durante agosto de 2020
- 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